cprover
|
#include <dependence_graph.h>
Public Types | |
typedef grapht< dep_nodet >::node_indext | node_indext |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
dep_graph_domaint () | |
bool | merge (const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to) |
void | transform (goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final override |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override |
jsont | output_json (const ai_baset &ai, const namespacet &ns) const override |
Outputs the current value of the domain. More... | |
void | make_top () final override |
void | make_bottom () final override |
void | make_entry () final override |
bool | is_top () const final override |
bool | is_bottom () const final override |
void | set_node_id (node_indext id) |
node_indext | get_node_id () const |
void | populate_dep_graph (dependence_grapht &, goto_programt::const_targett) const |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
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< goto_programt::const_targett > | depst |
Private Member Functions | |
void | control_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph) |
void | data_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns) |
Private Attributes | |
tvt | has_values |
node_indext | node_id |
bool | has_changed |
depst | control_deps |
depst | control_dep_candidates |
depst | data_deps |
Friends | |
const depst & | dependence_graph_test_get_control_deps (const dep_graph_domaint &) |
const depst & | dependence_graph_test_get_data_deps (const dep_graph_domaint &) |
Definition at line 66 of file dependence_graph.h.
|
private |
Definition at line 183 of file dependence_graph.h.
Definition at line 69 of file dependence_graph.h.
|
inline |
Definition at line 71 of file dependence_graph.h.
|
private |
Definition at line 55 of file dependence_graph.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, dependence_grapht::cfg_post_dominators(), control_dep_candidates, control_deps, cfg_dominators_templatet< P, T, post_dom >::nodet::dominators, cfg_baset< T, P, I >::entry_map, and INVARIANT.
Referenced by transform().
|
private |
Definition at line 153 of file dependence_graph.cpp.
References data_deps, forall_rw_range_set_r_objects, sparse_bitvector_analysist< V >::get(), rw_range_sett::get_ranges(), reaching_definitions_analysist::get_value_sets(), goto_rw(), may_be_def_use_pair(), and dependence_grapht::reaching_definitions().
Referenced by transform().
|
inline |
Definition at line 169 of file dependence_graph.h.
References node_id.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 150 of file dependence_graph.h.
References control_dep_candidates, control_deps, data_deps, DATA_INVARIANT, has_values, tvt::is_false(), and node_id.
Referenced by merge(), and transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 136 of file dependence_graph.h.
References control_dep_candidates, control_deps, data_deps, DATA_INVARIANT, has_values, tvt::is_true(), and node_id.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 109 of file dependence_graph.h.
References control_dep_candidates, control_deps, data_deps, DATA_INVARIANT, has_changed, has_values, and node_id.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 122 of file dependence_graph.h.
References control_dep_candidates, control_deps, data_deps, DATA_INVARIANT, has_changed, has_values, node_id, and tvt::unknown().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 98 of file dependence_graph.h.
References control_dep_candidates, control_deps, data_deps, DATA_INVARIANT, has_values, and node_id.
bool dep_graph_domaint::merge | ( | const dep_graph_domaint & | src, |
goto_programt::const_targett | from, | ||
goto_programt::const_targett | to | ||
) |
Definition at line 25 of file dependence_graph.cpp.
References control_dep_candidates, control_deps, data_deps, has_changed, has_values, is_bottom(), tvt::unknown(), and util_inplace_set_union().
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 238 of file dependence_graph.cpp.
References control_deps, and data_deps.
|
overridevirtual |
Outputs the current value of the domain.
Reimplemented from ai_domain_baset.
Definition at line 277 of file dependence_graph.cpp.
References control_deps, data_deps, json(), jsont::make_object(), json_arrayt::push_back(), and to_string().
void dep_graph_domaint::populate_dep_graph | ( | dependence_grapht & | dep_graph, |
goto_programt::const_targett | this_loc | ||
) | const |
Definition at line 322 of file dependence_graph.cpp.
References dependence_grapht::add_dep(), control_deps, dep_edget::CTRL, dep_edget::DATA, and data_deps.
|
inline |
Definition at line 164 of file dependence_graph.h.
References node_id.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 193 of file dependence_graph.cpp.
References control_dep_candidates, control_dependencies(), control_deps, data_dependencies(), dependence_grapht::get_state(), has_changed, has_values, is_bottom(), tvt::unknown(), and util_inplace_set_union().
|
friend |
|
friend |
|
private |
Definition at line 192 of file dependence_graph.h.
Referenced by control_dependencies(), is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and transform().
|
private |
Definition at line 187 of file dependence_graph.h.
Referenced by control_dependencies(), is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), output(), output_json(), populate_dep_graph(), and transform().
|
private |
Definition at line 196 of file dependence_graph.h.
Referenced by data_dependencies(), is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), output(), output_json(), and populate_dep_graph().
|
private |
Definition at line 181 of file dependence_graph.h.
Referenced by make_bottom(), make_entry(), merge(), and transform().
|
private |
Definition at line 179 of file dependence_graph.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and transform().
|
private |
Definition at line 180 of file dependence_graph.h.
Referenced by get_node_id(), is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), and set_node_id().