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, memory_modelt model) 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 72 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 70 of file event_graph.h.
typedef data_typet::value_type event_grapht::critical_cyclet::value_type |
Definition at line 74 of file event_graph.h.
|
inline |
Definition at line 98 of file event_graph.h.
|
inline |
Definition at line 93 of file event_graph.h.
Referenced by print_name().
|
inline |
Definition at line 94 of file event_graph.h.
|
inline |
Definition at line 76 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 77 of file event_graph.h.
|
inline |
Definition at line 78 of file event_graph.h.
|
inline |
Definition at line 82 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 147 of file event_graph.h.
References is_unsafe().
|
inline |
Definition at line 80 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 81 of file event_graph.h.
|
inline |
Definition at line 90 of file event_graph.h.
Referenced by check_AC(), and print_name().
|
inline |
Definition at line 91 of file event_graph.h.
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(), push_back(), and abstract_eventt::thread.
Referenced by event_grapht::graph_explorert::backtrack(), and print_name().
|
inline |
Definition at line 113 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 154 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 142 of file event_graph.h.
References is_unsafe().
|
inline |
Definition at line 103 of file event_graph.h.
References data, and has_user_defined_fence.
|
inline |
Definition at line 234 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 1127 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 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.
|
private |
Definition at line 1233 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 207 of file event_graph.h.
References print_name().
|
inline |
Definition at line 211 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 88 of file event_graph.h.
Referenced by hide_internals().
|
inline |
Definition at line 85 of file event_graph.h.
Referenced by event_grapht::graph_explorert::extract_cycle().
|
inline |
Definition at line 96 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 67 of file event_graph.h.
Referenced by event_grapht::graph_explorert::extract_cycle(), and operator()().
unsigned event_grapht::critical_cyclet::id |
Definition at line 66 of file event_graph.h.
std::set<delayt> event_grapht::critical_cyclet::unsafe_pairs |
Definition at line 200 of file event_graph.h.