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 |
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 &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 |
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 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 |
![]() | |
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 |
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< 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 &) |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
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 |
no states
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 |
a reasonable entry-point state
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 |
all states – the analysis doesn't use this, and domains may refuse to implement it.
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 |
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 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().