cprover
|
#include <reaching_definitions.h>
Public Types | |
typedef std::multimap< range_spect, range_spect > | rangest |
typedef std::map< locationt, rangest > | ranges_at_loct |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
rd_range_domaint () | |
void | set_bitvector_container (sparse_bitvector_analysist< reaching_definitiont > &_bv_container) |
void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override |
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... | |
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 |
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) |
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 |
![]() | |
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 &ns) 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::unordered_map< irep_idt, values_innert > | valuest |
typedef std::unordered_map< irep_idt, ranges_at_loct > | export_cachet |
Private Member Functions | |
void | populate_cache (const irep_idt &identifier) const |
void | transform_dead (const namespacet &ns, locationt from) |
void | transform_start_thread (const namespacet &ns, reaching_definitions_analysist &rd) |
void | transform_function_call (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd) |
void | transform_end_function (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd) |
void | transform_assign (const namespacet &ns, locationt from, 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) |
void | output (std::ostream &out) const |
bool | merge_inner (values_innert &dest, const values_innert &other) |
Private Attributes | |
tvt | has_values |
sparse_bitvector_analysist< reaching_definitiont > * | bv_container |
valuest | values |
export_cachet | export_cache |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
Definition at line 100 of file reaching_definitions.h.
|
private |
Definition at line 201 of file reaching_definitions.h.
typedef std::map<locationt, rangest> rd_range_domaint::ranges_at_loct |
Definition at line 177 of file reaching_definitions.h.
typedef std::multimap<range_spect, range_spect> rd_range_domaint::rangest |
Definition at line 176 of file reaching_definitions.h.
|
private |
Definition at line 190 of file reaching_definitions.h.
|
private |
Definition at line 194 of file reaching_definitions.h.
|
inline |
Definition at line 103 of file reaching_definitions.h.
|
inline |
Definition at line 180 of file reaching_definitions.h.
References export_cache.
Referenced by output().
|
private |
Definition at line 466 of file reaching_definitions.cpp.
References sparse_bitvector_analysist< V >::add(), reaching_definitiont::bit_begin, reaching_definitiont::bit_end, bv_container, reaching_definitiont::definition_at, export_cache, reaching_definitiont::identifier, and values.
Referenced by merge_inner(), transform_assign(), transform_end_function(), and transform_function_call().
const rd_range_domaint::ranges_at_loct & rd_range_domaint::get | ( | const irep_idt & | identifier | ) | const |
Definition at line 714 of file reaching_definitions.cpp.
References export_cache, and populate_cache().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 156 of file reaching_definitions.h.
References DATA_INVARIANT, has_values, tvt::is_false(), and values.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 149 of file reaching_definitions.h.
References DATA_INVARIANT, has_values, tvt::is_true(), and values.
|
private |
Definition at line 332 of file reaching_definitions.cpp.
References sparse_bitvector_analysist< V >::add(), reaching_definitiont::bit_begin, reaching_definitiont::bit_end, bv_container, export_cache, sparse_bitvector_analysist< V >::get(), kill_inf(), and values.
Referenced by transform(), transform_assign(), and transform_end_function().
|
private |
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 136 of file reaching_definitions.h.
References bv_container, sparse_bitvector_analysist< V >::clear(), has_values, and values.
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 144 of file reaching_definitions.h.
References 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 128 of file reaching_definitions.h.
References bv_container, sparse_bitvector_analysist< V >::clear(), has_values, and values.
Referenced by make_entry().
bool rd_range_domaint::merge | ( | const rd_range_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 629 of file reaching_definitions.cpp.
References export_cache, has_values, tvt::is_false(), merge_inner(), tvt::unknown(), and values.
|
private |
Definition at line 578 of file reaching_definitions.cpp.
References gen().
Referenced by merge(), and merge_shared().
bool rd_range_domaint::merge_shared | ( | const rd_range_domaint & | other, |
locationt | from, | ||
locationt | to, | ||
const namespacet & | ns | ||
) |
Definition at line 665 of file reaching_definitions.cpp.
References export_cache, has_values, tvt::is_false(), namespacet::lookup(), merge_inner(), tvt::unknown(), and values.
|
inlinefinaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 120 of file reaching_definitions.h.
|
private |
Definition at line 538 of file reaching_definitions.cpp.
References clear_cache(), has_values, tvt::is_known(), tvt::to_string(), and values.
|
private |
Definition at line 38 of file reaching_definitions.cpp.
References reaching_definitiont::bit_begin, reaching_definitiont::bit_end, bv_container, reaching_definitiont::definition_at, export_cache, sparse_bitvector_analysist< V >::get(), and values.
Referenced by get().
|
inline |
Definition at line 110 of file reaching_definitions.h.
References bv_container.
Referenced by reaching_definitions_analysist::get_state().
|
finaloverridevirtual |
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)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
Implements ai_domain_baset.
Definition at line 58 of file reaching_definitions.cpp.
References bv_container, forall_rw_range_set_w_objects, reaching_definitions_analysist::get_is_dirty(), reaching_definitions_analysist::get_is_threaded(), reaching_definitions_analysist::get_value_sets(), goto_rw(), INVARIANT_STRUCTURED, irept::is_not_nil(), symbolt::is_shared(), kill(), code_function_callt::lhs(), namespacet::lookup(), to_code_function_call(), transform_assign(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().
|
private |
Definition at line 296 of file reaching_definitions.cpp.
References forall_rw_range_set_w_objects, gen(), reaching_definitions_analysist::get_is_dirty(), reaching_definitions_analysist::get_is_threaded(), reaching_definitions_analysist::get_value_sets(), goto_rw(), INVARIANT_STRUCTURED, symbolt::is_shared(), kill(), and namespacet::lookup().
Referenced by transform(), transform_end_function(), and transform_function_call().
|
private |
Definition at line 127 of file reaching_definitions.cpp.
References export_cache, code_deadt::symbol(), to_code_dead(), to_symbol_expr(), and values.
Referenced by transform().
|
private |
Definition at line 228 of file reaching_definitions.cpp.
References reaching_definitiont::bit_begin, reaching_definitiont::bit_end, bv_container, reaching_definitiont::definition_at, dstringt::empty(), export_cache, gen(), sparse_bitvector_analysist< V >::get(), reaching_definitions_analysist::get_is_dirty(), reaching_definitions_analysist::get_is_threaded(), reaching_definitions_analysist::get_state(), reaching_definitiont::identifier, irept::is_not_nil(), kill(), code_function_callt::lhs(), namespacet::lookup(), code_typet::parameters(), to_code_function_call(), to_code_type(), transform_assign(), sparse_bitvector_analysist< V >::values, and values.
Referenced by transform().
|
private |
Definition at line 168 of file reaching_definitions.cpp.
References dstringt::empty(), export_cache, code_function_callt::function(), gen(), symbol_exprt::get_identifier(), reaching_definitions_analysist::get_is_dirty(), irept::is_not_nil(), symbolt::is_shared(), code_function_callt::lhs(), namespacet::lookup(), pointer_offset_bits(), to_code_function_call(), to_code_type(), to_range_spect(), to_symbol_expr(), transform_assign(), and values.
Referenced by transform().
|
private |
Definition at line 143 of file reaching_definitions.cpp.
References export_cache, reaching_definitions_analysist::get_is_dirty(), namespacet::lookup(), and values.
Referenced by transform().
|
private |
Definition at line 188 of file reaching_definitions.h.
Referenced by gen(), kill(), make_bottom(), make_top(), populate_cache(), set_bitvector_container(), transform(), and transform_end_function().
|
mutableprivate |
Definition at line 203 of file reaching_definitions.h.
Referenced by clear_cache(), gen(), get(), kill(), merge(), merge_shared(), populate_cache(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().
|
private |
Definition at line 186 of file reaching_definitions.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_top(), merge(), merge_shared(), and output().
|
private |
Definition at line 196 of file reaching_definitions.h.
Referenced by gen(), is_bottom(), is_top(), kill(), kill_inf(), make_bottom(), make_top(), merge(), merge_shared(), output(), populate_cache(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().