cprover
|
#include <event_graph.h>
Classes | |
struct | delayt |
Public Member Functions | |
critical_cyclet (event_grapht &_egraph, unsigned _id) | |
void | operator() (const critical_cyclet &cyc) |
bool | is_cycle () |
void | hide_internals (critical_cyclet &reduced) const |
bool | is_unsafe (memory_modelt model, bool fast=false) |
checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set More... | |
bool | is_unsafe_fast (memory_modelt model) |
void | compute_unsafe_pairs (memory_modelt model) |
bool | is_unsafe_asm (memory_modelt model, bool fast=false) |
same as is_unsafe, but with ASM fences More... | |
bool | is_not_uniproc (memory_modelt model) const |
bool | is_not_thin_air () const |
std::string | print () const |
std::string | print_events () const |
std::string | print_name (memory_modelt model) const |
std::string | print_name (memory_modelt model, bool hide_internals) const |
std::string | print_unsafes () const |
std::string | print_output () const |
std::string | print_all (memory_modelt model, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, bool hide_internals) const |
void | print_dot (std::ostream &str, unsigned colour, memory_modelt model) const |
bool | operator< (const critical_cyclet &other) const |
Public Attributes | |
unsigned | id |
bool | has_user_defined_fence |
std::set< delayt > | unsafe_pairs |
Protected Member Functions | |
bool | is_not_uniproc () const |
bool | is_not_weak_uniproc () const |
std::string | print_detail (const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, memory_modelt model) const |
std::string | print_name (const critical_cyclet &redyced, memory_modelt model) const |
bool | check_AC (const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const |
bool | check_BC (const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const |
Protected Attributes | |
event_grapht & | egraph |
Definition at line 38 of file event_graph.h.
|
inline |
Definition at line 63 of file event_graph.h.
|
protected |
Definition at line 186 of file event_graph.cpp.
References egraph, abstract_eventt::Fence, abstract_eventt::operation, and abstract_eventt::thread.
|
protected |
Definition at line 227 of file event_graph.cpp.
References abstract_eventt::Fence, abstract_eventt::operation, and abstract_eventt::thread.
|
inline |
Definition at line 110 of file event_graph.h.
References is_unsafe().
void event_grapht::critical_cyclet::hide_internals | ( | critical_cyclet & | reduced | ) | const |
Definition at line 1157 of file event_graph.cpp.
References abstract_eventt::is_fence(), and abstract_eventt::thread.
Referenced by event_grapht::graph_explorert::backtrack(), and print_name().
|
inline |
Definition at line 76 of file event_graph.h.
References event_grapht::are_po_ordered(), egraph, and event_grapht::size().
Referenced by event_grapht::graph_explorert::backtrack().
bool event_grapht::critical_cyclet::is_not_thin_air | ( | ) | const |
Definition at line 970 of file event_graph.cpp.
References data_dpt::dp(), abstract_eventt::operation, abstract_eventt::Read, event_grapht::size(), abstract_eventt::thread, and abstract_eventt::Write.
Referenced by event_grapht::graph_explorert::backtrack().
|
protected |
Definition at line 895 of file event_graph.cpp.
References abstract_eventt::ASMfence, abstract_eventt::Fence, id2string(), abstract_eventt::Lwfence, abstract_eventt::operation, and abstract_eventt::variable.
Referenced by event_grapht::graph_explorert::backtrack(), and is_not_uniproc().
|
inline |
Definition at line 117 of file event_graph.h.
References is_not_uniproc(), is_not_weak_uniproc(), and RMO.
|
protected |
Definition at line 933 of file event_graph.cpp.
References abstract_eventt::ASMfence, abstract_eventt::Fence, abstract_eventt::Lwfence, abstract_eventt::operation, abstract_eventt::Read, and abstract_eventt::variable.
Referenced by is_not_uniproc().
bool event_grapht::critical_cyclet::is_unsafe | ( | memory_modelt | model, |
bool | fast = false |
||
) |
checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set
Definition at line 280 of file event_graph.cpp.
References data_dpt::dp(), messaget::eom(), abstract_eventt::Fence, abstract_eventt::Lwfence, abstract_eventt::operation, Power, event_grapht::size(), abstract_eventt::thread, abstract_eventt::unsafe_pair(), abstract_eventt::unsafe_pair_lwfence(), and abstract_eventt::variable.
Referenced by event_grapht::graph_explorert::backtrack(), compute_unsafe_pairs(), and is_unsafe_fast().
bool event_grapht::critical_cyclet::is_unsafe_asm | ( | memory_modelt | model, |
bool | fast = false |
||
) |
same as is_unsafe, but with ASM fences
Definition at line 562 of file event_graph.cpp.
References abstract_eventt::ASMfence, data_dpt::dp(), messaget::eom(), Power, event_grapht::size(), abstract_eventt::thread, abstract_eventt::unsafe_pair(), and abstract_eventt::unsafe_pair_asm().
|
inline |
Definition at line 105 of file event_graph.h.
References is_unsafe().
|
inline |
Definition at line 68 of file event_graph.h.
References event_grapht::clear(), and has_user_defined_fence.
|
inline |
Definition at line 197 of file event_graph.h.
std::string event_grapht::critical_cyclet::print | ( | ) | const |
Definition at line 1018 of file event_graph.cpp.
std::string event_grapht::critical_cyclet::print_all | ( | memory_modelt | model, |
std::map< std::string, std::string > & | map_id2var, | ||
std::map< std::string, std::string > & | map_var2id, | ||
bool | hide_internals | ||
) | const |
Definition at line 1127 of file event_graph.cpp.
References event_grapht::size().
|
protected |
Definition at line 1098 of file event_graph.cpp.
References source_locationt::as_string(), id2string(), abstract_eventt::source_location, abstract_eventt::thread, and abstract_eventt::variable.
void event_grapht::critical_cyclet::print_dot | ( | std::ostream & | str, |
unsigned | colour, | ||
memory_modelt | model | ||
) | const |
Definition at line 1538 of file event_graph.cpp.
References abstract_eventt::Fence, abstract_eventt::get_operation(), abstract_eventt::id, abstract_eventt::Lwfence, abstract_eventt::operation, Power, print_colour, abstract_eventt::Read, abstract_eventt::thread, abstract_eventt::variable, and abstract_eventt::Write.
std::string event_grapht::critical_cyclet::print_events | ( | ) | const |
Definition at line 1073 of file event_graph.cpp.
References abstract_eventt::get_operation(), id2string(), and abstract_eventt::variable.
|
protected |
Definition at line 1233 of file event_graph.cpp.
References abstract_eventt::ASMfence, data_dpt::dp(), abstract_eventt::Fence, abstract_eventt::fence_value(), abstract_eventt::get_operation(), abstract_eventt::Lwfence, abstract_eventt::operation, Power, abstract_eventt::Read, size_type(), abstract_eventt::thread, abstract_eventt::variable, and abstract_eventt::Write.
Referenced by event_grapht::graph_explorert::backtrack(), and print_name().
|
inline |
Definition at line 170 of file event_graph.h.
References print_name().
|
inline |
Definition at line 174 of file event_graph.h.
References egraph, hide_internals(), and print_name().
std::string event_grapht::critical_cyclet::print_output | ( | ) | const |
Definition at line 1085 of file event_graph.cpp.
References source_locationt::as_string(), id2string(), abstract_eventt::source_location, abstract_eventt::thread, and abstract_eventt::variable.
std::string event_grapht::critical_cyclet::print_unsafes | ( | ) | const |
Definition at line 1026 of file event_graph.cpp.
References abstract_eventt::Fence, abstract_eventt::get_operation(), abstract_eventt::operation, abstract_eventt::Read, abstract_eventt::thread, abstract_eventt::variable, and abstract_eventt::Write.
|
protected |
Definition at line 41 of file event_graph.h.
Referenced by check_AC(), is_cycle(), and print_name().
bool event_grapht::critical_cyclet::has_user_defined_fence |
Definition at line 61 of file event_graph.h.
Referenced by fence_user_def_insertert::contains_user_def(), event_grapht::graph_explorert::extract_cycle(), and operator()().
unsigned event_grapht::critical_cyclet::id |
Definition at line 59 of file event_graph.h.
std::set<delayt> event_grapht::critical_cyclet::unsafe_pairs |
Definition at line 163 of file event_graph.h.
Referenced by cycles_visitort::com_constraint(), cycles_visitort::porr_constraint(), cycles_visitort::porw_constraint(), cycles_visitort::powr_constraint(), and cycles_visitort::poww_constraint().