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 |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
void | make_top () final |
void | make_bottom () final |
void | make_entry () 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 |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
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 |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Private Types | |
typedef std::set< std::size_t > | values_innert |
typedef std::unordered_map< irep_idt, values_innert, irep_id_hash > | valuest |
typedef std::unordered_map< irep_idt, ranges_at_loct, irep_id_hash > | 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 |
Definition at line 100 of file reaching_definitions.h.
|
private |
Definition at line 190 of file reaching_definitions.h.
typedef std::map<locationt, rangest> rd_range_domaint::ranges_at_loct |
Definition at line 165 of file reaching_definitions.h.
typedef std::multimap<range_spect, range_spect> rd_range_domaint::rangest |
Definition at line 164 of file reaching_definitions.h.
|
private |
Definition at line 178 of file reaching_definitions.h.
|
private |
Definition at line 182 of file reaching_definitions.h.
|
inline |
Definition at line 103 of file reaching_definitions.h.
|
inline |
Definition at line 168 of file reaching_definitions.h.
Referenced by output().
|
private |
Definition at line 457 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 705 of file reaching_definitions.cpp.
References export_cache, and populate_cache().
|
private |
Definition at line 323 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 |
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 138 of file reaching_definitions.h.
References sparse_bitvector_analysist< V >::values.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 146 of file reaching_definitions.h.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 130 of file reaching_definitions.h.
References sparse_bitvector_analysist< V >::values.
bool rd_range_domaint::merge | ( | const rd_range_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 620 of file reaching_definitions.cpp.
References export_cache, has_values, tvt::is_false(), merge_inner(), tvt::unknown(), and values.
|
private |
Definition at line 569 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 656 of file reaching_definitions.cpp.
References export_cache, has_values, tvt::is_false(), namespacet::lookup(), merge_inner(), tvt::unknown(), and values.
|
inlinefinalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 122 of file reaching_definitions.h.
|
private |
Definition at line 529 of file reaching_definitions.cpp.
References clear_cache(), has_values, tvt::is_known(), tvt::to_string(), and values.
|
private |
Definition at line 26 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.
Referenced by reaching_definitions_analysist::get_state().
|
final |
Definition at line 46 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 287 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 115 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 219 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 156 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 131 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 176 of file reaching_definitions.h.
Referenced by gen(), kill(), populate_cache(), transform(), and transform_end_function().
|
mutableprivate |
Definition at line 192 of file reaching_definitions.h.
Referenced by gen(), get(), kill(), merge(), merge_shared(), populate_cache(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().
|
private |
Definition at line 174 of file reaching_definitions.h.
Referenced by merge(), merge_shared(), and output().
|
private |
Definition at line 184 of file reaching_definitions.h.
Referenced by gen(), kill(), kill_inf(), merge(), merge_shared(), output(), populate_cache(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().