Loading...

Searching...

No Matches

rd_range_domaint Class Reference

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:

[フレーム]

[legend]

+ Collaboration diagram for rd_range_domaint:

[フレーム]

[legend]

Public Types

typedef std::multimap< range_spect, range_spect > rangest

typedef std::map< locationt, rangest, goto_programt::target_less_than > 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, message_handlert &message_handler)

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.

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 directly (see make_entry) and domains may refuse to implement it.

void make_bottom () final override

no states

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.

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 void make_entry ()

Make this domain a reasonable entry-point state For most domains top is sufficient.

virtual bool ai_simplify (exprt &condition, const namespacet &) const

also add

virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const

Simplifies the expression but keeps it as an l-value.

virtual exprt to_predicate (void) const

Gives a Boolean condition that is true for all values represented by the domain.

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

void transform_dead (const namespacet &ns, locationt from)

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

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.

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.

sparse_bitvector_analysist< reaching_definitiont > *const bv_container

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

valuest values

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

export_cachet export_cache

It is a helper data structure.

message_handlert & message_handler

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.

ai_domain_baset (const ai_domain_baset &old)

A copy constructor is part of the domain interface.

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 158 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 285 of file reaching_definitions.h.

◆ ranges_at_loct

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

Definition at line 253 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 276 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,

message_handlert & message_handler

)

inline

Definition at line 161 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 256 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 481 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 721 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 343 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 443 of file reaching_definitions.cpp.

◆ make_bottom()

void rd_range_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 208 of file reaching_definitions.h.

◆ make_top()

void rd_range_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 200 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 636 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 586 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 672 of file reaching_definitions.cpp.

◆ output() [1/2]

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

private

Definition at line 546 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 192 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 73 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 93 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 305 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 138 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 243 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 178 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 153 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 274 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 297 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 265 of file reaching_definitions.h.

◆ message_handler

message_handlert& rd_range_domaint::message_handler

private

Definition at line 346 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 283 of file reaching_definitions.h.

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

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