cprover
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, rangestranges_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, locationt from, const irep_idt &function_to, locationt 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, locationt from, locationt 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 void transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
 how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...
 
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_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...
 

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

Member Typedef Documentation

◆ export_cachet

Definition at line 271 of file reaching_definitions.h.

◆ ranges_at_loct

Definition at line 234 of file reaching_definitions.h.

◆ rangest

Definition at line 233 of file reaching_definitions.h.

◆ values_innert

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

Definition at line 257 of file reaching_definitions.h.

◆ valuest

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

Definition at line 259 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 139 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 237 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 509 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 757 of file reaching_definitions.cpp.

◆ is_bottom()

bool rd_range_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 202 of file reaching_definitions.h.

◆ is_top()

bool rd_range_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 195 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 371 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 471 of file reaching_definitions.cpp.

◆ make_bottom()

void rd_range_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 182 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 190 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 174 of file reaching_definitions.h.

◆ merge()

bool rd_range_domaint::merge ( const rd_range_domaint other,
locationt  from,
locationt  to 
)

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

It operates only onthis->valuesandother.values<tt>. The keys in the resulting map is the union of variable names in boththis->valuesand other.values<tt>. And for each variablevappearing in both maps this->valuesandother.values<tt>the resulting mapped set ofIDs is the set union ofthis->values[v]andother.values[v]. NOTE: The operation actually does not produce a newjoinelement. The instance*thisis modified to become thejoinelement. \param other: The instance to be merged into*this` as the join operation

Parameters
fromNot used at all.
toNot used at all.
Returns
Returns true iff there is something new
returns true iff there is something new

Definition at line 672 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 621 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 708 of file reaching_definitions.cpp.

◆ output() [1/2]

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

Definition at line 581 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 166 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,
locationt  from,
const irep_idt function_to,
locationt  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.
fromReference to a GOTO instruction according to which *this instance should be transformed.
function_toJust passed to transform_function_call callee.
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 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 334 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 164 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 265 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 204 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 179 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 255 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 286 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 246 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 268 of file reaching_definitions.h.


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