cprover
fence_user_def_insertert Class Reference

#include <fence_user_def.h>

Inheritance diagram for fence_user_def_insertert:
[legend]
Collaboration diagram for fence_user_def_insertert:
[legend]

Public Member Functions

 fence_user_def_insertert (instrumentert &instr)
 
 fence_user_def_insertert (instrumentert &instr, memory_modelt _model)
 
- Public Member Functions inherited from fence_insertert
unsigned add_edge (const edget &e)
 
unsigned add_invisible_edge (const edget &e)
 
 fence_insertert (instrumentert &instr)
 
 fence_insertert (instrumentert &instr, memory_modelt _model)
 
void compute ()
 
void print_to_file ()
 
void print_to_file_2 ()
 
void print_to_file_3 ()
 
void print_to_file_4 ()
 
typet get_type (const irep_idt &id)
 
typet type_component (std::list< std::string >::const_iterator it, std::list< std::string >::const_iterator end, const typet &type)
 

Protected Member Functions

bool contains_user_def (const event_grapht::critical_cyclet &cycle) const
 
virtual void process_cycles_selection ()
 
virtual bool filter_cycles (unsigned cycles_id) const
 
- Protected Member Functions inherited from fence_insertert
void mip_set_var (ilpt &ilp, unsigned &i)
 
void mip_set_cst (ilpt &ilp, unsigned &i)
 
void mip_fill_matrix (ilpt &ilp, unsigned &i, unsigned const_constraints_number, unsigned const_unique)
 
void preprocess ()
 
void solve ()
 
virtual unsigned fence_cost (fence_typet e) const
 
std::string to_string (fence_typet f) const
 
unsigned col_to_var (unsigned u) const
 
fence_typet col_to_fence (unsigned u) const
 
unsigned var_fence_to_col (fence_typet f, unsigned var) const
 
void import_freq ()
 
void compute_fence_options ()
 
void print_vars () const
 

Protected Attributes

std::set< unsigned > selected_cycles
 
- Protected Attributes inherited from fence_insertert
unsigned & unique
 
unsigned fence_options
 
mip_vart var
 
mip_vart invisible_var
 
std::set< event_idtpo
 
std::list< std::set< event_idt > > powr_constraints
 
std::list< std::set< event_idt > > poww_constraints
 
std::list< std::set< event_idt > > porw_constraints
 
std::list< std::set< event_idt > > porr_constraints
 
std::list< std::set< event_idt > > com_constraints
 
cycles_visitort cycles_visitor
 
const float epsilon
 
const bool with_freq
 
std::map< unsigned, float > freq_table
 
std::map< edget, fence_typetfenced_edges
 

Additional Inherited Members

- Public Types inherited from fence_insertert
typedef event_grapht::critical_cyclet::delayt edget
 
- Static Public Member Functions inherited from fence_insertert
static std::string remove_extra (const irep_idt &id)
 
static std::string remove_extra (std::string copy)
 
- Public Attributes inherited from fence_insertert
instrumentertinstrumenter
 
std::map< unsigned, edget > & map_to_e
 normal variables used almost every time More...
 
std::map< edget, unsigned > & map_from_e
 
std::size_t constraints_number
 number of constraints More...
 
const memory_modelt model
 
const_graph_visitort const_graph_visitor
 to retrieve the concrete graph edges involved in the (abstract) cycles More...
 
- Protected Types inherited from fence_insertert
enum  fence_typet {
  Fence =0, Dp =1, Lwfence =2, Branching =3,
  Ctlfence =4
}
 

Detailed Description

Definition at line 24 of file fence_user_def.h.

Constructor & Destructor Documentation

◆ fence_user_def_insertert() [1/2]

fence_user_def_insertert::fence_user_def_insertert ( instrumentert instr)
inlineexplicit

Definition at line 41 of file fence_user_def.h.

◆ fence_user_def_insertert() [2/2]

fence_user_def_insertert::fence_user_def_insertert ( instrumentert instr,
memory_modelt  _model 
)
inline

Definition at line 46 of file fence_user_def.h.

Member Function Documentation

◆ contains_user_def()

bool fence_user_def_insertert::contains_user_def ( const event_grapht::critical_cyclet cycle) const
protected

◆ filter_cycles()

virtual bool fence_user_def_insertert::filter_cycles ( unsigned  cycles_id) const
inlineprotectedvirtual

Reimplemented from fence_insertert.

Definition at line 35 of file fence_user_def.h.

References selected_cycles.

◆ process_cycles_selection()

void fence_user_def_insertert::process_cycles_selection ( )
protectedvirtual

Member Data Documentation

◆ selected_cycles

std::set<unsigned> fence_user_def_insertert::selected_cycles
protected

Definition at line 27 of file fence_user_def.h.

Referenced by filter_cycles(), and process_cycles_selection().


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