cprover
fence_insertert Class Reference

#include <fence_inserter.h>

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

Public Types

typedef event_grapht::critical_cyclet::delayt edget
 

Public Member Functions

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 ()
 
virtual void process_cycles_selection ()
 
virtual bool filter_cycles (unsigned cycle_id) const
 
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)
 

Static Public Member Functions

static std::string remove_extra (const irep_idt &id)
 
static std::string remove_extra (std::string copy)
 

Public Attributes

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

enum  fence_typet {
  Fence =0, Dp =1, Lwfence =2, Branching =3,
  Ctlfence =4
}
 

Protected Member Functions

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

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
 

Detailed Description

Definition at line 60 of file fence_inserter.h.

Member Typedef Documentation

§ edget

Member Enumeration Documentation

§ fence_typet

Enumerator
Fence 
Dp 
Lwfence 
Branching 
Ctlfence 

Definition at line 106 of file fence_inserter.h.

Constructor & Destructor Documentation

§ fence_insertert() [1/2]

fence_insertert::fence_insertert ( instrumentert instr)
inlineexplicit

Definition at line 144 of file fence_inserter.h.

§ fence_insertert() [2/2]

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

Definition at line 152 of file fence_inserter.h.

Member Function Documentation

§ add_edge()

§ add_invisible_edge()

unsigned fence_insertert::add_invisible_edge ( const edget e)
inline

Definition at line 71 of file fence_inserter.h.

Referenced by cycles_visitort::com_constraint().

§ col_to_fence()

fence_insertert::fence_typet fence_insertert::col_to_fence ( unsigned  u) const
inlineprotected

Definition at line 975 of file fence_inserter.cpp.

References Branching, Ctlfence, Dp, Fence, fence_options, and Lwfence.

Referenced by mip_fill_matrix(), and solve().

§ col_to_var()

unsigned fence_insertert::col_to_var ( unsigned  u) const
inlineprotected

Definition at line 970 of file fence_inserter.cpp.

References fence_options.

Referenced by mip_fill_matrix(), mip_set_var(), and solve().

§ compute()

§ compute_fence_options()

void fence_insertert::compute_fence_options ( )
protected

Definition at line 1003 of file fence_inserter.cpp.

References fence_options, model, Power, PSO, RMO, TSO, and Unknown.

Referenced by compute().

§ fence_cost()

unsigned fence_insertert::fence_cost ( fence_typet  e) const
protectedvirtual

Definition at line 28 of file fence_inserter.cpp.

References Branching, Ctlfence, Dp, Fence, and Lwfence.

Referenced by mip_set_var().

§ filter_cycles()

virtual bool fence_insertert::filter_cycles ( unsigned  cycle_id) const
inlinevirtual

Reimplemented in fence_assert_insertert, and fence_user_def_insertert.

Definition at line 167 of file fence_inserter.h.

Referenced by mip_set_var(), cycles_visitort::po_edges(), and preprocess().

§ get_type()

typet fence_insertert::get_type ( const irep_idt id)

§ import_freq()

void fence_insertert::import_freq ( )
protected

Definition at line 812 of file fence_inserter.cpp.

§ mip_fill_matrix()

§ mip_set_cst()

void fence_insertert::mip_set_cst ( ilpt ilp,
unsigned &  i 
)
inlineprotected

§ mip_set_var()

void fence_insertert::mip_set_var ( ilpt ilp,
unsigned &  i 
)
inlineprotected

§ preprocess()

§ print_to_file()

§ print_to_file_2()

§ print_to_file_3()

§ print_to_file_4()

§ print_vars()

void fence_insertert::print_vars ( ) const
protected

§ process_cycles_selection()

virtual void fence_insertert::process_cycles_selection ( )
inlinevirtual

Reimplemented in fence_assert_insertert, and fence_user_def_insertert.

Definition at line 166 of file fence_inserter.h.

Referenced by preprocess().

§ remove_extra() [1/2]

static std::string fence_insertert::remove_extra ( const irep_idt id)
inlinestatic

Definition at line 176 of file fence_inserter.h.

References id2string().

§ remove_extra() [2/2]

static std::string fence_insertert::remove_extra ( std::string  copy)
inlinestatic

Definition at line 182 of file fence_inserter.h.

References get_type().

§ solve()

§ to_string()

std::string fence_insertert::to_string ( fence_typet  f) const
protected

Definition at line 957 of file fence_inserter.cpp.

References Branching, Ctlfence, Dp, Fence, and Lwfence.

Referenced by print_to_file(), print_to_file_2(), print_to_file_3(), print_to_file_4(), and solve().

§ type_component()

typet fence_insertert::type_component ( std::list< std::string >::const_iterator  it,
std::list< std::string >::const_iterator  end,
const typet type 
)

Definition at line 1085 of file fence_inserter.cpp.

References struct_union_typet::component_type(), irept::id(), and to_struct_union_type().

Referenced by get_type().

§ var_fence_to_col()

unsigned fence_insertert::var_fence_to_col ( fence_typet  f,
unsigned  var 
) const
inlineprotected

Definition at line 989 of file fence_inserter.cpp.

References Branching, Ctlfence, Dp, Fence, fence_options, and Lwfence.

Referenced by mip_fill_matrix().

Member Data Documentation

§ com_constraints

std::list<std::set<event_idt> > fence_insertert::com_constraints
protected

Definition at line 117 of file fence_inserter.h.

Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().

§ const_graph_visitor

const_graph_visitort fence_insertert::const_graph_visitor

to retrieve the concrete graph edges involved in the (abstract) cycles

Definition at line 81 of file fence_inserter.h.

Referenced by mip_fill_matrix(), cycles_visitort::po_edges(), and preprocess().

§ constraints_number

§ cycles_visitor

cycles_visitort fence_insertert::cycles_visitor
protected

Definition at line 120 of file fence_inserter.h.

Referenced by preprocess().

§ epsilon

const float fence_insertert::epsilon
protected

Definition at line 128 of file fence_inserter.h.

Referenced by mip_set_var().

§ fence_options

unsigned fence_insertert::fence_options
protected

§ fenced_edges

std::map<edget, fence_typet> fence_insertert::fenced_edges
protected

§ freq_table

std::map<unsigned, float> fence_insertert::freq_table
protected

Definition at line 130 of file fence_inserter.h.

Referenced by mip_set_var().

§ instrumenter

§ invisible_var

mip_vart fence_insertert::invisible_var
protected

Definition at line 91 of file fence_inserter.h.

Referenced by mip_fill_matrix(), preprocess(), and print_vars().

§ map_from_e

std::map<edget, unsigned>& fence_insertert::map_from_e

Definition at line 69 of file fence_inserter.h.

Referenced by print_vars(), and const_graph_visitort::PT().

§ map_to_e

std::map<unsigned, edget>& fence_insertert::map_to_e

normal variables used almost every time

Definition at line 68 of file fence_inserter.h.

Referenced by mip_fill_matrix(), preprocess(), and solve().

§ model

const memory_modelt fence_insertert::model

§ po

std::set<event_idt> fence_insertert::po
protected

Definition at line 112 of file fence_inserter.h.

Referenced by preprocess().

§ porr_constraints

std::list<std::set<event_idt> > fence_insertert::porr_constraints
protected

Definition at line 116 of file fence_inserter.h.

Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().

§ porw_constraints

std::list<std::set<event_idt> > fence_insertert::porw_constraints
protected

Definition at line 115 of file fence_inserter.h.

Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().

§ powr_constraints

std::list<std::set<event_idt> > fence_insertert::powr_constraints
protected

Definition at line 113 of file fence_inserter.h.

Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().

§ poww_constraints

std::list<std::set<event_idt> > fence_insertert::poww_constraints
protected

Definition at line 114 of file fence_inserter.h.

Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().

§ unique

unsigned& fence_insertert::unique
protected

Definition at line 84 of file fence_inserter.h.

Referenced by compute(), mip_fill_matrix(), mip_set_var(), and solve().

§ var

mip_vart fence_insertert::var
protected

Definition at line 88 of file fence_inserter.h.

§ with_freq

const bool fence_insertert::with_freq
protected

Definition at line 129 of file fence_inserter.h.

Referenced by mip_set_var().


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