CBMC
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:
+ Collaboration diagram for rd_range_domaint:

Public Types

typedef std::multimap< range_spect, range_spectrangest
 
typedef std::map< locationt, rangest, goto_programt::target_less_thanranges_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. 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 directly (see make_entry) and domains may refuse to implement it. More...
 
void make_bottom () final override
 no states 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_loctget (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. More...
 
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_innertvaluest
 
typedef std::map< irep_idt, ranges_at_loctexport_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 IDs of reaching_definitiont instances stored in map pointed to by bv_container. More...
 
export_cachet export_cache
 It is a helper data structure. More...
 
message_handlertmessage_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. 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 158 of file reaching_definitions.h.

Member Typedef Documentation

◆ export_cachet

Definition at line 285 of file reaching_definitions.h.

◆ ranges_at_loct

◆ 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
otherThe instance to be merged into *this as the join operation
fromNot used at all.
toNot 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_fromJust passed to transform_function_call and transform_end_function callees.
trace_fromThe ai_history giving the GOTO instruction which *this instance should be transformed.
function_toJust passed to transform_function_call callee.
trace_toJust passed to transform_end_function callee.
aiA reference to 'reaching_definitions_analysist' instance.
nsJust 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: