cprover
|
#include <event_graph.h>
Classes | |
class | critical_cyclet |
class | graph_conc_explorert |
class | graph_explorert |
class | graph_pensieve_explorert |
Public Attributes | |
bool | filter_thin_air |
bool | filter_uniproc |
messaget & | message |
std::map< unsigned, data_dpt > | map_data_dp |
std::list< event_idt > | po_order |
std::list< event_idt > | poUrfe_order |
std::set< std::pair< event_idt, event_idt > > | loops |
std::set< std::pair< const abstract_eventt &, const abstract_eventt & > > | duplicated_bodies |
Protected Attributes | |
wmm_grapht | po_graph |
wmm_grapht | com_graph |
unsigned | max_var |
unsigned | max_po_trans |
bool | ignore_arrays |
Definition at line 34 of file event_graph.h.
|
inlineexplicit |
Definition at line 347 of file event_graph.h.
Definition at line 435 of file event_graph.h.
References grapht< N >::add_edge(), com_graph, and poUrfe_order.
Referenced by add_undirected_com_edge(), copy_segment(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
inline |
Definition at line 367 of file event_graph.h.
References grapht< N >::add_node(), com_graph, and po_graph.
Referenced by copy_segment(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
Definition at line 424 of file event_graph.h.
References grapht< N >::add_edge(), loops, po_graph, po_order, and poUrfe_order.
Referenced by instrumentert::cfg_visitort::visit_cfg_backedge().
Definition at line 415 of file event_graph.h.
References grapht< N >::add_edge(), po_graph, po_order, and poUrfe_order.
Referenced by copy_segment(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
Definition at line 442 of file event_graph.h.
References add_com_edge().
Definition at line 481 of file event_graph.h.
References loops, and po_order.
Referenced by event_grapht::critical_cyclet::is_cycle(), and cycles_visitort::po_edges().
|
inline |
Definition at line 500 of file event_graph.h.
References grapht< N >::clear(), com_graph, map_data_dp, and po_graph.
Referenced by event_grapht::critical_cyclet::operator()().
|
inline |
Definition at line 513 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles(), max_po_trans, and max_var.
Referenced by instrumentert::collect_cycles(), and instrumentert::collect_cycles_by_SCCs().
|
inline |
Definition at line 521 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles(), max_po_trans, and max_var.
|
inline |
Definition at line 540 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs(), max_po_trans, and max_var.
Referenced by instrumenter_pensievet::collect_pairs().
|
inline |
Definition at line 546 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs(), max_po_trans, max_var, and event_grapht::graph_pensieve_explorert::set_naive().
Referenced by instrumenter_pensievet::collect_pairs_naive().
|
inline |
Definition at line 405 of file event_graph.h.
References com_graph, and grapht< N >::in().
|
inline |
Definition at line 410 of file event_graph.h.
References com_graph, and grapht< N >::out().
Referenced by event_grapht::graph_pensieve_explorert::collect_pairs(), and print_rec_graph().
Definition at line 90 of file event_graph.cpp.
References add_com_edge(), add_node(), add_po_edge(), duplicated_bodies, messaget::eom(), explore_copy_segment(), source_locationt::get_file(), source_locationt::get_function(), has_com_edge(), has_po_edge(), message, operator[](), size(), abstract_eventt::source_location, and messaget::status().
Referenced by instrumentert::cfg_visitort::visit_cfg_duplicate().
void event_grapht::explore_copy_segment | ( | std::set< event_idt > & | explored, |
event_idt | begin, | ||
event_idt | end | ||
) | const |
copies the segment
begin | top of the subgraph |
end | bottom of the subgraph |
Definition at line 72 of file event_graph.cpp.
References po_out().
Referenced by copy_segment().
Definition at line 385 of file event_graph.h.
References com_graph, and grapht< N >::has_edge().
Referenced by copy_segment().
Definition at line 380 of file event_graph.h.
References grapht< N >::has_edge(), and po_graph.
Referenced by const_graph_visitort::const_graph_explore(), copy_segment(), and const_graph_visitort::graph_explore().
|
inline |
Definition at line 475 of file event_graph.h.
References operator[]().
|
inline |
Definition at line 375 of file event_graph.h.
References po_graph.
Referenced by copy_segment(), is_local(), and print_rec_graph().
|
inline |
Definition at line 395 of file event_graph.h.
References grapht< N >::in(), and po_graph.
Referenced by const_graph_visitort::const_graph_explore_AC(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), const_graph_visitort::graph_explore_AC(), and cycles_visitort::po_edges().
|
inline |
Definition at line 400 of file event_graph.h.
References grapht< N >::out(), and po_graph.
Referenced by const_graph_visitort::const_graph_explore(), const_graph_visitort::const_graph_explore_BC(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), explore_copy_segment(), const_graph_visitort::graph_explore(), const_graph_visitort::graph_explore_BC(), instrumentert::is_cfg_spurious(), cycles_visitort::po_edges(), print_rec_graph(), and const_graph_visitort::PT().
void event_grapht::print_graph | ( | ) |
Definition at line 56 of file event_graph.cpp.
References po_order, and print_rec_graph().
Referenced by fence_weak_memory().
void event_grapht::print_rec_graph | ( | std::ofstream & | file, |
event_idt | node_id, | ||
std::set< event_idt > & | visited | ||
) |
Definition at line 28 of file event_graph.cpp.
References com_out(), operator[](), po_out(), and abstract_eventt::source_location.
Referenced by print_graph().
Definition at line 454 of file event_graph.h.
References com_graph, and grapht< N >::remove_edge().
Referenced by remove_edge().
Definition at line 459 of file event_graph.h.
References remove_com_edge(), and remove_po_edge().
Definition at line 449 of file event_graph.h.
References po_graph, and grapht< N >::remove_edge().
Referenced by remove_edge().
|
inline |
Definition at line 528 of file event_graph.h.
References ignore_arrays, max_po_trans, and max_var.
Referenced by instrumentert::set_parameters_collection().
|
inline |
Definition at line 390 of file event_graph.h.
References po_graph, and grapht< N >::size().
Referenced by copy_segment(), event_grapht::critical_cyclet::is_cycle(), event_grapht::critical_cyclet::is_not_thin_air(), event_grapht::critical_cyclet::is_unsafe(), event_grapht::critical_cyclet::is_unsafe_asm(), and event_grapht::critical_cyclet::print_all().
|
protected |
Definition at line 206 of file event_graph.h.
Referenced by add_com_edge(), add_node(), clear(), com_in(), com_out(), has_com_edge(), and remove_com_edge().
std::set<std::pair<const abstract_eventt&, const abstract_eventt&> > event_grapht::duplicated_bodies |
Definition at line 473 of file event_graph.h.
Referenced by copy_segment().
bool event_grapht::filter_thin_air |
Definition at line 354 of file event_graph.h.
Referenced by event_grapht::graph_explorert::collect_cycles().
bool event_grapht::filter_uniproc |
Definition at line 355 of file event_graph.h.
|
protected |
Definition at line 211 of file event_graph.h.
Referenced by set_parameters_collection().
Definition at line 365 of file event_graph.h.
Referenced by add_po_back_edge(), and are_po_ordered().
std::map<unsigned, data_dpt> event_grapht::map_data_dp |
Definition at line 359 of file event_graph.h.
Referenced by clear(), and instrumentert::cfg_visitort::visit_cfg_function().
|
protected |
Definition at line 210 of file event_graph.h.
Referenced by event_grapht::graph_explorert::collect_cycles(), collect_cycles(), collect_pairs(), collect_pairs_naive(), and set_parameters_collection().
|
protected |
Definition at line 209 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), collect_cycles(), collect_pairs(), collect_pairs_naive(), and set_parameters_collection().
messaget& event_grapht::message |
Definition at line 356 of file event_graph.h.
Referenced by event_grapht::graph_pensieve_explorert::collect_pairs(), copy_segment(), event_grapht::graph_explorert::filter_thin_air(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
protected |
Definition at line 205 of file event_graph.h.
Referenced by add_node(), add_po_back_edge(), add_po_edge(), clear(), has_po_edge(), operator[](), po_in(), po_out(), remove_po_edge(), and size().
std::list<event_idt> event_grapht::po_order |
Definition at line 362 of file event_graph.h.
Referenced by add_po_back_edge(), add_po_edge(), are_po_ordered(), event_grapht::graph_pensieve_explorert::collect_pairs(), and print_graph().
std::list<event_idt> event_grapht::poUrfe_order |
Definition at line 363 of file event_graph.h.
Referenced by add_com_edge(), add_po_back_edge(), and add_po_edge().