cprover
|
#include <event_graph.h>
Classes | |
struct | delayt |
Public Types | |
typedef data_typet::iterator | iterator |
typedef data_typet::const_iterator | const_iterator |
typedef data_typet::value_type | value_type |
Public Member Functions | |
iterator | begin () |
const_iterator | begin () const |
const_iterator | cbegin () const |
iterator | end () |
const_iterator | end () const |
const_iterator | cend () const |
template<typename T > | |
void | push_front (T &&t) |
template<typename T > | |
void | push_back (T &&t) |
value_type & | front () |
const value_type & | front () const |
value_type & | back () |
const value_type & | back () const |
size_t | size () const |
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 |
Private Types | |
typedef std::list< event_idt > | data_typet |
Private 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) const |
std::string | print_name (const critical_cyclet &redyced, memory_modelt model) const |
bool | check_AC (data_typet::const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const |
bool | check_BC (data_typet::const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const |
Private Attributes | |
data_typet | data |
event_grapht & | egraph |
Definition at line 39 of file event_graph.h.
typedef data_typet::const_iterator event_grapht::critical_cyclet::const_iterator |
Definition at line 71 of file event_graph.h.
|
private |
Definition at line 41 of file event_graph.h.
typedef data_typet::iterator event_grapht::critical_cyclet::iterator |
Definition at line 69 of file event_graph.h.
typedef data_typet::value_type event_grapht::critical_cyclet::value_type |
Definition at line 73 of file event_graph.h.
|
inline |
Definition at line 97 of file event_graph.h.
|
inline |
Definition at line 92 of file event_graph.h.
Referenced by print_name().
|
inline |
Definition at line 93 of file event_graph.h.
|
inline |
Definition at line 75 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), check_AC(), instrumentert::is_cfg_spurious(), print_detail(), and print_name().
|
inline |
Definition at line 76 of file event_graph.h.
|
inline |
Definition at line 77 of file event_graph.h.
|
inline |
Definition at line 81 of file event_graph.h.
|
private |
Definition at line 186 of file event_graph.cpp.
References begin(), egraph, end(), abstract_eventt::Fence, front(), abstract_eventt::operation, and abstract_eventt::thread.
|
private |
Definition at line 227 of file event_graph.cpp.
References abstract_eventt::Fence, abstract_eventt::operation, and abstract_eventt::thread.
|
inline |
Definition at line 146 of file event_graph.h.
References is_unsafe().
|
inline |
Definition at line 79 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), check_AC(), instrumentert::is_cfg_spurious(), print_detail(), and print_name().
|
inline |
Definition at line 80 of file event_graph.h.
|
inline |
Definition at line 89 of file event_graph.h.
Referenced by check_AC(), and print_name().
|
inline |
Definition at line 90 of file event_graph.h.
void event_grapht::critical_cyclet::hide_internals | ( | critical_cyclet & | reduced | ) | const |
Definition at line 1156 of file event_graph.cpp.
References abstract_eventt::is_fence(), push_back(), and abstract_eventt::thread.
Referenced by event_grapht::graph_explorert::backtrack(), and print_name().
|
inline |
Definition at line 112 of file event_graph.h.
References event_grapht::are_po_ordered(), egraph, and data::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().
|
private |
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 153 of file event_graph.h.
References is_not_uniproc(), is_not_weak_uniproc(), and RMO.
|
private |
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 141 of file event_graph.h.
References is_unsafe().
|
inline |
Definition at line 102 of file event_graph.h.
References data, and has_user_defined_fence.
|
inline |
Definition at line 233 of file event_graph.h.
References data.
std::string event_grapht::critical_cyclet::print | ( | ) | const |
Definition at line 1018 of file event_graph.cpp.
References to_string().
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 1126 of file event_graph.cpp.
References size(), and event_grapht::size().
|
private |
Definition at line 1098 of file event_graph.cpp.
References source_locationt::as_string(), begin(), end(), id2string(), abstract_eventt::source_location, abstract_eventt::thread, to_string(), and abstract_eventt::variable.
void event_grapht::critical_cyclet::print_dot | ( | std::ostream & | str, |
unsigned | colour, | ||
memory_modelt | model | ||
) | const |
Definition at line 1537 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.
|
private |
Definition at line 1232 of file event_graph.cpp.
References abstract_eventt::ASMfence, back(), begin(), data_dpt::dp(), end(), abstract_eventt::Fence, abstract_eventt::fence_value(), front(), abstract_eventt::get_operation(), abstract_eventt::Lwfence, abstract_eventt::operation, Power, abstract_eventt::Read, size(), 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 206 of file event_graph.h.
References print_name().
|
inline |
Definition at line 210 of file event_graph.h.
References data, egraph, hide_internals(), INVARIANT, 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, to_string(), 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.
|
inline |
Definition at line 87 of file event_graph.h.
Referenced by hide_internals().
|
inline |
Definition at line 84 of file event_graph.h.
Referenced by event_grapht::graph_explorert::extract_cycle().
|
inline |
Definition at line 95 of file event_graph.h.
References data::size.
Referenced by print_all(), and print_name().
|
private |
Definition at line 42 of file event_graph.h.
Referenced by operator()(), operator<(), and print_name().
|
private |
Definition at line 44 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 66 of file event_graph.h.
Referenced by event_grapht::graph_explorert::extract_cycle(), and operator()().
unsigned event_grapht::critical_cyclet::id |
Definition at line 65 of file event_graph.h.
std::set<delayt> event_grapht::critical_cyclet::unsafe_pairs |
Definition at line 199 of file event_graph.h.