cprover
event_grapht::critical_cyclet Class Referencefinal

#include <event_graph.h>

Collaboration diagram for event_grapht::critical_cyclet:
[legend]

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_typefront ()
 
const value_typefront () const
 
value_typeback ()
 
const value_typeback () 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< delaytunsafe_pairs
 

Private Types

typedef std::list< event_idtdata_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_graphtegraph
 

Detailed Description

Definition at line 39 of file event_graph.h.

Member Typedef Documentation

◆ const_iterator

typedef data_typet::const_iterator event_grapht::critical_cyclet::const_iterator

Definition at line 72 of file event_graph.h.

◆ data_typet

Definition at line 41 of file event_graph.h.

◆ iterator

typedef data_typet::iterator event_grapht::critical_cyclet::iterator

Definition at line 70 of file event_graph.h.

◆ value_type

typedef data_typet::value_type event_grapht::critical_cyclet::value_type

Definition at line 74 of file event_graph.h.

Constructor & Destructor Documentation

◆ critical_cyclet()

event_grapht::critical_cyclet::critical_cyclet ( event_grapht _egraph,
unsigned  _id 
)
inline

Definition at line 98 of file event_graph.h.

Member Function Documentation

◆ back() [1/2]

value_type& event_grapht::critical_cyclet::back ( )
inline

Definition at line 93 of file event_graph.h.

Referenced by print_name().

◆ back() [2/2]

const value_type& event_grapht::critical_cyclet::back ( ) const
inline

Definition at line 94 of file event_graph.h.

◆ begin() [1/2]

iterator event_grapht::critical_cyclet::begin ( )
inline

◆ begin() [2/2]

const_iterator event_grapht::critical_cyclet::begin ( ) const
inline

Definition at line 77 of file event_graph.h.

◆ cbegin()

const_iterator event_grapht::critical_cyclet::cbegin ( ) const
inline

Definition at line 78 of file event_graph.h.

◆ cend()

const_iterator event_grapht::critical_cyclet::cend ( ) const
inline

Definition at line 82 of file event_graph.h.

◆ check_AC()

bool event_grapht::critical_cyclet::check_AC ( data_typet::const_iterator  s_it,
const abstract_eventt first,
const abstract_eventt second 
) const
private

◆ check_BC()

bool event_grapht::critical_cyclet::check_BC ( data_typet::const_iterator  it,
const abstract_eventt first,
const abstract_eventt second 
) const
private

◆ compute_unsafe_pairs()

void event_grapht::critical_cyclet::compute_unsafe_pairs ( memory_modelt  model)
inline

Definition at line 147 of file event_graph.h.

References is_unsafe().

◆ end() [1/2]

iterator event_grapht::critical_cyclet::end ( )
inline

◆ end() [2/2]

const_iterator event_grapht::critical_cyclet::end ( ) const
inline

Definition at line 81 of file event_graph.h.

◆ front() [1/2]

value_type& event_grapht::critical_cyclet::front ( )
inline

Definition at line 90 of file event_graph.h.

Referenced by check_AC(), and print_name().

◆ front() [2/2]

const value_type& event_grapht::critical_cyclet::front ( ) const
inline

Definition at line 91 of file event_graph.h.

◆ hide_internals()

void event_grapht::critical_cyclet::hide_internals ( critical_cyclet reduced) const

◆ is_cycle()

bool event_grapht::critical_cyclet::is_cycle ( )
inline

◆ is_not_thin_air()

bool event_grapht::critical_cyclet::is_not_thin_air ( ) const

◆ is_not_uniproc() [1/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( ) const
private

◆ is_not_uniproc() [2/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( memory_modelt  model) const
inline

Definition at line 154 of file event_graph.h.

References is_not_uniproc(), is_not_weak_uniproc(), and RMO.

◆ is_not_weak_uniproc()

bool event_grapht::critical_cyclet::is_not_weak_uniproc ( ) const
private

◆ is_unsafe()

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().

◆ is_unsafe_asm()

bool event_grapht::critical_cyclet::is_unsafe_asm ( memory_modelt  model,
bool  fast = false 
)

◆ is_unsafe_fast()

bool event_grapht::critical_cyclet::is_unsafe_fast ( memory_modelt  model)
inline

Definition at line 142 of file event_graph.h.

References is_unsafe().

◆ operator()()

void event_grapht::critical_cyclet::operator() ( const critical_cyclet cyc)
inline

Definition at line 103 of file event_graph.h.

References data, and has_user_defined_fence.

◆ operator<()

bool event_grapht::critical_cyclet::operator< ( const critical_cyclet other) const
inline

Definition at line 234 of file event_graph.h.

References data.

◆ print()

std::string event_grapht::critical_cyclet::print ( ) const

Definition at line 1018 of file event_graph.cpp.

References to_string().

◆ print_all()

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().

◆ print_detail()

std::string event_grapht::critical_cyclet::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
private

◆ print_dot()

void event_grapht::critical_cyclet::print_dot ( std::ostream &  str,
unsigned  colour,
memory_modelt  model 
) const

◆ print_events()

std::string event_grapht::critical_cyclet::print_events ( ) const

◆ print_name() [1/3]

◆ print_name() [2/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt  model) const
inline

Definition at line 207 of file event_graph.h.

References print_name().

◆ print_name() [3/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt  model,
bool  hide_internals 
) const
inline

Definition at line 211 of file event_graph.h.

References data, egraph, hide_internals(), INVARIANT, and print_name().

◆ print_output()

std::string event_grapht::critical_cyclet::print_output ( ) const

◆ print_unsafes()

std::string event_grapht::critical_cyclet::print_unsafes ( ) const

◆ push_back()

template<typename T >
void event_grapht::critical_cyclet::push_back ( T &&  t)
inline

Definition at line 88 of file event_graph.h.

Referenced by hide_internals().

◆ push_front()

template<typename T >
void event_grapht::critical_cyclet::push_front ( T &&  t)
inline

Definition at line 85 of file event_graph.h.

Referenced by event_grapht::graph_explorert::extract_cycle().

◆ size()

size_t event_grapht::critical_cyclet::size ( ) const
inline

Definition at line 96 of file event_graph.h.

References data::size.

Referenced by print_all(), and print_name().

Member Data Documentation

◆ data

data_typet event_grapht::critical_cyclet::data
private

Definition at line 42 of file event_graph.h.

Referenced by operator()(), operator<(), and print_name().

◆ egraph

event_grapht& event_grapht::critical_cyclet::egraph
private

Definition at line 44 of file event_graph.h.

Referenced by check_AC(), is_cycle(), and print_name().

◆ has_user_defined_fence

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()().

◆ id

unsigned event_grapht::critical_cyclet::id

Definition at line 66 of file event_graph.h.

◆ unsafe_pairs

std::set<delayt> event_grapht::critical_cyclet::unsafe_pairs

Definition at line 200 of file event_graph.h.


The documentation for this class was generated from the following files: