CBMC
|
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>
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 . 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_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. 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_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... | |
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. More... | |
ai_domain_baset (const ai_domain_baset &old) | |
A copy constructor is part of the domain interface. More... | |
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.
|
private |
Definition at line 285 of file reaching_definitions.h.
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.
typedef std::multimap<range_spect, range_spect> rd_range_domaint::rangest |
Definition at line 251 of file reaching_definitions.h.
|
private |
Definition at line 276 of file reaching_definitions.h.
|
private |
Definition at line 277 of file reaching_definitions.h.
|
inline |
Definition at line 161 of file reaching_definitions.h.
|
inline |
Definition at line 256 of file reaching_definitions.h.
|
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.
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.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 223 of file reaching_definitions.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 216 of file reaching_definitions.h.
|
private |
Definition at line 343 of file reaching_definitions.cpp.
|
private |
Definition at line 443 of file reaching_definitions.cpp.
|
inlinefinaloverridevirtual |
|
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.
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.
other | The instance to be merged into *this as the join operation |
from | Not used at all. |
to | Not used at all. |
Definition at line 636 of file reaching_definitions.cpp.
|
private |
Definition at line 586 of file reaching_definitions.cpp.
bool rd_range_domaint::merge_shared | ( | const rd_range_domaint & | other, |
locationt | from, | ||
locationt | to, | ||
const namespacet & | ns | ||
) |
Definition at line 672 of file reaching_definitions.cpp.
|
private |
Definition at line 546 of file reaching_definitions.cpp.
|
inlinefinaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 192 of file reaching_definitions.h.
|
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.
|
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.
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.
|
private |
Definition at line 305 of file reaching_definitions.cpp.
|
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.
|
private |
Definition at line 243 of file reaching_definitions.cpp.
|
private |
Definition at line 178 of file reaching_definitions.cpp.
|
private |
Definition at line 153 of file reaching_definitions.cpp.
|
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.
|
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 ID
s 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.
|
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.
|
private |
Definition at line 346 of file reaching_definitions.h.
|
private |
It is an ordered map from program variable names to ID
s 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.