Because the class is inherited from ai_domain_baset, its instance represents an element of a domain of the reaching definitions abstract interpretation analysis. More...

#include <reaching_definitions.h>

Inheritance diagram for rd_range_domaint:

Collaboration diagram for rd_range_domaint:

Public Types
typedef std::multimap< range_spect, range_spect >	rangest

typedef std::map< locationt, rangest >	ranges_at_loct

Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Public Member Functions
	rd_range_domaint (sparse_bitvector_analysist< reaching_definitiont > *_bv_container)

void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
	Computes an instance obtained from the instance `*this` by transformation over a GOTO instruction referenced by `from`. More...

void	output (std::ostream &out, const ai_baset &, const namespacet &) const final override

void	make_top () final override
	all states – the analysis doesn't use this, and domains may refuse to implement it. More...

void	make_bottom () final override
	no states More...

void	make_entry () final override
	Make this domain a reasonable entry-point state. More...

bool	is_top () const override final

bool	is_bottom () const override final

bool	merge (const rd_range_domaint &other, trace_ptrt from, trace_ptrt to)
	Implements the "join" operation of two instances `*this` and `other`. More...

bool	merge_shared (const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)

const ranges_at_loct &	get (const irep_idt &identifier) const

void	clear_cache (const irep_idt &identifier) const

Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()

virtual jsont	output_json (const ai_baset &ai, const namespacet &ns) const

virtual xmlt	output_xml (const ai_baset &ai, const namespacet &ns) const

virtual bool	ai_simplify (exprt &condition, const namespacet &) const
	also add More...

virtual bool	ai_simplify_lhs (exprt &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value. More...

virtual exprt	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain. More...

Private Types
typedef std::set< std::size_t >	values_innert

typedef std::map< irep_idt, values_innert >	valuest

typedef std::map< irep_idt, ranges_at_loct >	export_cachet

Private Member Functions
void	populate_cache (const irep_idt &identifier) const
	Given the passed variable name `identifier` it collects data from `bv_container` for each `ID` in `values[identifier]` and stores them into `export_cache[identifier]`. More...

void	transform_dead (const namespacet &ns, locationt from)
	Computes an instance obtained from a `*this` by transformation over `DEAD v` GOTO instruction. More...

void	transform_start_thread (const namespacet &ns, reaching_definitions_analysist &rd)

void	transform_function_call (const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)

void	transform_end_function (const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)

void	transform_assign (const namespacet &ns, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)

void	kill (const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)

void	kill_inf (const irep_idt &identifier, const range_spect &range_start)

bool	gen (locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
	A utility function which updates internal data structures by inserting a new reaching definition record, for the variable name `identifier`, written in given GOTO instruction referenced by `from`, at the range of bits defined by `range_start` and `range_end`. More...

void	output (std::ostream &out) const

bool	merge_inner (values_innert &dest, const values_innert &other)

Private Attributes
tvt	has_values
	This (three value logic) flag determines, whether the instance represents `top`, `bottom`, or any other element of the lattice, by values `TRUE`, `FALSE`, and `UNKNOWN` respectively. More...

sparse_bitvector_analysist< reaching_definitiont > *const	bv_container
	It points to the actual reaching definitions data of individual program variables. More...

valuest	values
	It is an ordered map from program variable names to `ID`s of `reaching_definitiont` instances stored in map pointed to by `bv_container`. More...

export_cachet	export_cache
	It is a helper data structure. More...

Additional Inherited Members
Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...

	ai_domain_baset (const ai_domain_baset &old)
	A copy constructor is part of the domain interface. More...

Detailed Description

Because the class is inherited from ai_domain_baset, its instance represents an element of a domain of the reaching definitions abstract interpretation analysis.

Each instance is thus associated with exactly one instruction in an analysed GOTO program. And so, the instance holds information for individual program variables about their reaching definitions, at that instruction.

Definition at line 157 of file reaching_definitions.h.

Member Typedef Documentation

◆ export_cachet

typedef std::map<irep_idt, ranges_at_loct> rd_range_domaint::export_cachet

private

Definition at line 289 of file reaching_definitions.h.

◆ ranges_at_loct

typedef std::map<locationt, rangest> rd_range_domaint::ranges_at_loct

Definition at line 252 of file reaching_definitions.h.

◆ rangest

typedef std::multimap<range_spect, range_spect> rd_range_domaint::rangest

Definition at line 251 of file reaching_definitions.h.

◆ values_innert

typedef std::set<std::size_t> rd_range_domaint::values_innert

private

Definition at line 275 of file reaching_definitions.h.

◆ valuest

typedef std::map<irep_idt, values_innert> rd_range_domaint::valuest

private

Definition at line 277 of file reaching_definitions.h.

Constructor & Destructor Documentation

◆ rd_range_domaint()

rd_range_domaint::rd_range_domaint ( sparse_bitvector_analysist< reaching_definitiont > * _bv_container )

inline

Definition at line 160 of file reaching_definitions.h.

Member Function Documentation

◆ clear_cache()

void rd_range_domaint::clear_cache ( const irep_idt & identifier ) const

inline

Definition at line 255 of file reaching_definitions.h.

◆ gen()

bool rd_range_domaint::gen	(	locationt	from,
		const irep_idt &	identifier,
		const range_spect &	range_start,
		const range_spect &	range_end
	)

private

A utility function which updates internal data structures by inserting a new reaching definition record, for the variable name identifier, written in given GOTO instruction referenced by from, at the range of bits defined by range_start and range_end.

Definition at line 479 of file reaching_definitions.cpp.

◆ get()

const rd_range_domaint::ranges_at_loct & rd_range_domaint::get ( const irep_idt & identifier ) const

Definition at line 719 of file reaching_definitions.cpp.

◆ is_bottom()

bool rd_range_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 223 of file reaching_definitions.h.

◆ is_top()

bool rd_range_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 216 of file reaching_definitions.h.

◆ kill()

void rd_range_domaint::kill	(	const irep_idt &	identifier,
		const range_spect &	range_start,
		const range_spect &	range_end
	)

private

Definition at line 341 of file reaching_definitions.cpp.

◆ kill_inf()

void rd_range_domaint::kill_inf	(	const irep_idt &	identifier,
		const range_spect &	range_start
	)

private

Definition at line 441 of file reaching_definitions.cpp.

◆ make_bottom()

void rd_range_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 203 of file reaching_definitions.h.

◆ make_entry()

void rd_range_domaint::make_entry ( )

inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 211 of file reaching_definitions.h.

◆ make_top()

void rd_range_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 195 of file reaching_definitions.h.

◆ merge()

bool rd_range_domaint::merge	(	const rd_range_domaint &	other,
		trace_ptrt	from,
		trace_ptrt	to
	)

Implements the "join" operation of two instances *this and other.

It operates only on this->values and other.values. The keys in the resulting map are the union of variable names in both this->values and other.values. For each variable v appearing in both maps this->values and other.values the resulting mapped set of identifiers is the set union of this->values[v] and other.values[v]. Note that the operation actually does not produce a new join element. The instance *this is modified to become the join element.

Parameters

other	The instance to be merged into `*this` as the join operation
from	Not used at all.
to	Not used at all.

Returns: Returns true iff there is something new

Definition at line 634 of file reaching_definitions.cpp.

◆ merge_inner()

bool rd_range_domaint::merge_inner	(	values_innert &	dest,
		const values_innert &	other
	)

private

Returns: returns true iff there is something new

Definition at line 584 of file reaching_definitions.cpp.

◆ merge_shared()

bool rd_range_domaint::merge_shared	(	const rd_range_domaint &	other,
		locationt	from,
		locationt	to,
		const namespacet &	ns
	)

Returns: returns true iff there is something new

Definition at line 670 of file reaching_definitions.cpp.

◆ output() [1/2]

void rd_range_domaint::output ( std::ostream & out ) const

private

Definition at line 544 of file reaching_definitions.cpp.

◆ output() [2/2]

void rd_range_domaint::output	(	std::ostream &	out,
		const ai_baset &	,
		const namespacet &
	)		const

inlinefinaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 187 of file reaching_definitions.h.

◆ populate_cache()

void rd_range_domaint::populate_cache ( const irep_idt & identifier ) const

private

Given the passed variable name identifier it collects data from bv_container for each ID in values[identifier] and stores them into export_cache[identifier].

Namely, for each reaching_definitiont instance rd obtained from bv_container it associates rd.definition_at with the bit-range (rd.bit_begin, rd.bit_end).

This function is only used to fill in the cache export_cache for the output method.

Definition at line 71 of file reaching_definitions.cpp.

◆ transform()

void rd_range_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	trace_from,
		const irep_idt &	function_to,
		trace_ptrt	trace_to,
		ai_baset &	ai,
		const namespacet &	ns
	)

finaloverridevirtual

Computes an instance obtained from the instance *this by transformation over a GOTO instruction referenced by from.

The method implements a switch according to a type of the instruction and then calls a dedicated transform_* method for the recognised instruction.

Parameters

function_from	Just passed to `transform_function_call` and `transform_end_function` callees.
trace_from	The ai_history giving the GOTO instruction which `*this` instance should be transformed.
function_to	Just passed to `transform_function_call` callee.
trace_to	Just passed to `transform_end_function` callee.
ai	A reference to 'reaching_definitions_analysist' instance.
ns	Just passed to callees.

Implements ai_domain_baset.

Definition at line 91 of file reaching_definitions.cpp.

◆ transform_assign()

void rd_range_domaint::transform_assign	(	const namespacet &	ns,
		locationt	from,
		const irep_idt &	function_to,
		locationt	to,
		reaching_definitions_analysist &	rd
	)

private

Definition at line 303 of file reaching_definitions.cpp.

◆ transform_dead()

void rd_range_domaint::transform_dead	(	const namespacet &	ns,
		locationt	from
	)

private

Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.

The operation simply removes v from this->values.

Definition at line 136 of file reaching_definitions.cpp.

◆ transform_end_function()

void rd_range_domaint::transform_end_function	(	const namespacet &	ns,
		const irep_idt &	function_from,
		locationt	from,
		const irep_idt &	function_to,
		locationt	to,
		reaching_definitions_analysist &	rd
	)

private

Definition at line 241 of file reaching_definitions.cpp.

◆ transform_function_call()

void rd_range_domaint::transform_function_call	(	const namespacet &	ns,
		const irep_idt &	function_from,
		locationt	from,
		const irep_idt &	function_to,
		reaching_definitions_analysist &	rd
	)

private

Definition at line 176 of file reaching_definitions.cpp.

◆ transform_start_thread()

void rd_range_domaint::transform_start_thread	(	const namespacet &	ns,
		reaching_definitions_analysist &	rd
	)

private

Definition at line 151 of file reaching_definitions.cpp.

Member Data Documentation

◆ bv_container

sparse_bitvector_analysist<reaching_definitiont>* const rd_range_domaint::bv_container

private

It points to the actual reaching definitions data of individual program variables.

This pointer is initially nullptr and it is later set (by reaching_definitions_analysist instance using the method set_bitvector_container) to a valid pointer, which is actually shared by all rd_range_domaint instances. NOTE: reaching_definitions_analysist inherits from sparse_bitvector_analysist<reaching_definitiont> and so this is passed to set_bitvector_container for all instances.

Definition at line 273 of file reaching_definitions.h.

◆ export_cache

export_cachet rd_range_domaint::export_cache

mutableprivate

It is a helper data structure.

It consists of data already stored in values and bv_container. It is basically (an ordered) map from (a subset of) variables in values to iterators to GOTO instructions where the variables are defined. Moreover, each such iterator is also associated with a range of bits defining the value of that variable at that GOTO instruction. Both the iterators and the corresponding bit ranges are simply taken from reaching_definitiont instances obtained for IDs in values[var_name]. This data structure is actually used only in the output method; other methods only remove outdated data from it. Since the cache does not contribute to the computation, it should be either moved to the output method or removed entirely.

Definition at line 304 of file reaching_definitions.h.

◆ has_values

tvt rd_range_domaint::has_values

private

This (three value logic) flag determines, whether the instance represents top, bottom, or any other element of the lattice, by values TRUE, FALSE, and UNKNOWN respectively.

Initially it is set to FALSE.

Definition at line 264 of file reaching_definitions.h.

◆ values

valuest rd_range_domaint::values

private

It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in map pointed to by bv_container.

The map is not empty only if has_value is UNKNOWN. Variables in the map are all those which are live at the associated instruction.

Definition at line 286 of file reaching_definitions.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/reaching_definitions.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/reaching_definitions.cpp

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ export_cachet

◆ ranges_at_loct

◆ rangest

◆ values_innert

◆ valuest

Constructor & Destructor Documentation

◆ rd_range_domaint()

Member Function Documentation

◆ clear_cache()

◆ gen()

◆ get()

◆ is_bottom()

◆ is_top()

◆ kill()

◆ kill_inf()

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ merge()

◆ merge_inner()

◆ merge_shared()

◆ output() [1/2]

◆ output() [2/2]

◆ populate_cache()

◆ transform()

◆ transform_assign()

◆ transform_dead()

◆ transform_end_function()

◆ transform_function_call()

◆ transform_start_thread()

Member Data Documentation

◆ bv_container

◆ export_cache

◆ has_values

◆ values