cprover
|
#include <fence_inserter.h>
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 | |
instrumentert & | instrumenter |
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_idt > | po |
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_typet > | fenced_edges |
Definition at line 60 of file fence_inserter.h.
Definition at line 63 of file fence_inserter.h.
|
protected |
Enumerator | |
---|---|
Fence | |
Dp | |
Lwfence | |
Branching | |
Ctlfence |
Definition at line 106 of file fence_inserter.h.
|
inlineexplicit |
Definition at line 144 of file fence_inserter.h.
|
inline |
Definition at line 152 of file fence_inserter.h.
|
inline |
Definition at line 70 of file fence_inserter.h.
Referenced by const_graph_visitort::const_graph_explore(), const_graph_visitort::const_graph_explore_AC(), const_graph_visitort::const_graph_explore_BC(), const_graph_visitort::graph_explore(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), cycles_visitort::po_edges(), cycles_visitort::porr_constraint(), cycles_visitort::porw_constraint(), cycles_visitort::powr_constraint(), and cycles_visitort::poww_constraint().
|
inline |
Definition at line 71 of file fence_inserter.h.
Referenced by cycles_visitort::com_constraint().
|
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().
|
inlineprotected |
Definition at line 970 of file fence_inserter.cpp.
References fence_options.
Referenced by mip_fill_matrix(), mip_set_var(), and solve().
void fence_insertert::compute | ( | ) |
Definition at line 47 of file fence_inserter.cpp.
References compute_fence_options(), messaget::eom(), instrumenter, instrumentert::message, preprocess(), messaget::result(), solve(), messaget::status(), and unique.
Referenced by fence_weak_memory().
|
protected |
Definition at line 1003 of file fence_inserter.cpp.
References fence_options, model, Power, PSO, RMO, TSO, and Unknown.
Referenced by compute().
|
protectedvirtual |
Definition at line 28 of file fence_inserter.cpp.
References Branching, Ctlfence, Dp, Fence, and Lwfence.
Referenced by mip_set_var().
|
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().
Definition at line 1040 of file fence_inserter.cpp.
References messaget::debug(), messaget::eom(), id2string(), instrumenter, namespacet::lookup(), instrumentert::message, instrumentert::ns, and type_component().
Referenced by print_to_file_4().
|
protected |
Definition at line 812 of file fence_inserter.cpp.
|
inlineprotected |
Definition at line 406 of file fence_inserter.cpp.
References Branching, col_to_fence(), col_to_var(), com_constraints, const_graph_visitor, const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), Ctlfence, messaget::debug(), Dp, messaget::eom(), Fence, fence_options, instrumenter, invisible_var, Lwfence, mip_vart::map_to_e, map_to_e, instrumentert::message, model, porr_constraints, porw_constraints, Power, powr_constraints, poww_constraints, const_graph_visitort::PT(), messaget::statistics(), unique, Unknown, and var_fence_to_col().
Referenced by solve().
|
inlineprotected |
Definition at line 312 of file fence_inserter.cpp.
References com_constraints, constraints_number, model, porr_constraints, porw_constraints, Power, powr_constraints, poww_constraints, and Unknown.
Referenced by solve().
|
inlineprotected |
Definition at line 210 of file fence_inserter.cpp.
References Branching, col_to_var(), Ctlfence, Dp, epsilon, Fence, fence_cost(), fence_options, filter_cycles(), freq_table, instrumenter, Lwfence, model, Power, instrumentert::set_of_cycles, unique, Unknown, and with_freq.
Referenced by solve().
|
protected |
Definition at line 59 of file fence_inserter.cpp.
References cycles_visitort::com_constraint(), com_constraints, const_graph_visitor, const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), cycles_visitor, messaget::eom(), filter_cycles(), instrumenter, invisible_var, mip_vart::map_to_e, map_to_e, instrumentert::message, model, po, cycles_visitort::po_edges(), cycles_visitort::porr_constraint(), porr_constraints, cycles_visitort::porw_constraint(), porw_constraints, Power, cycles_visitort::powr_constraint(), powr_constraints, cycles_visitort::poww_constraint(), poww_constraints, process_cycles_selection(), const_graph_visitort::PT(), instrumentert::set_of_cycles, messaget::status(), and Unknown.
Referenced by compute().
void fence_insertert::print_to_file | ( | ) |
Definition at line 817 of file fence_inserter.cpp.
References instrumentert::egraph, fenced_edges, source_locationt::get_column(), source_locationt::get_file(), source_locationt::get_line(), instrumenter, abstract_eventt::source_location, and to_string().
void fence_insertert::print_to_file_2 | ( | ) |
Definition at line 844 of file fence_inserter.cpp.
References instrumentert::egraph, fenced_edges, source_locationt::get_file(), source_locationt::get_line(), instrumenter, abstract_eventt::source_location, and to_string().
void fence_insertert::print_to_file_3 | ( | ) |
Definition at line 873 of file fence_inserter.cpp.
References instrumentert::egraph, messaget::eom(), fenced_edges, source_locationt::get_file(), source_locationt::get_function(), source_locationt::get_line(), instrumenter, instrumentert::message, abstract_eventt::source_location, to_string(), abstract_eventt::variable, and messaget::warning().
Referenced by fence_weak_memory().
void fence_insertert::print_to_file_4 | ( | ) |
Definition at line 914 of file fence_inserter.cpp.
References instrumentert::egraph, messaget::eom(), fenced_edges, irept::get(), source_locationt::get_file(), source_locationt::get_function(), source_locationt::get_line(), get_type(), instrumenter, instrumentert::message, abstract_eventt::source_location, to_string(), abstract_eventt::variable, and messaget::warning().
|
protected |
Definition at line 1021 of file fence_inserter.cpp.
References messaget::eom(), instrumenter, invisible_var, mip_vart::map_from_e, map_from_e, instrumentert::message, and messaget::statistics().
Referenced by solve().
|
inlinevirtual |
Reimplemented in fence_assert_insertert, and fence_user_def_insertert.
Definition at line 166 of file fence_inserter.h.
Referenced by preprocess().
|
inlinestatic |
Definition at line 176 of file fence_inserter.h.
References id2string().
|
inlinestatic |
Definition at line 182 of file fence_inserter.h.
References get_type().
|
protected |
Definition at line 703 of file fence_inserter.cpp.
References col_to_fence(), col_to_var(), constraints_number, messaget::debug(), instrumentert::egraph, messaget::eom(), fence_options, fenced_edges, instrumenter, map_to_e, instrumentert::message, mip_fill_matrix(), mip_set_cst(), mip_set_var(), print_vars(), messaget::result(), instrumentert::set_of_cycles, messaget::statistics(), to_string(), and unique.
Referenced by compute().
|
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().
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().
|
inlineprotected |
Definition at line 989 of file fence_inserter.cpp.
References Branching, Ctlfence, Dp, Fence, fence_options, and Lwfence.
Referenced by mip_fill_matrix().
|
protected |
Definition at line 117 of file fence_inserter.h.
Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().
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().
std::size_t fence_insertert::constraints_number |
number of constraints
Definition at line 77 of file fence_inserter.h.
Referenced by cycles_visitort::com_constraint(), mip_set_cst(), cycles_visitort::porr_constraint(), cycles_visitort::porw_constraint(), cycles_visitort::powr_constraint(), cycles_visitort::poww_constraint(), and solve().
|
protected |
Definition at line 120 of file fence_inserter.h.
Referenced by preprocess().
|
protected |
Definition at line 128 of file fence_inserter.h.
Referenced by mip_set_var().
|
protected |
Definition at line 85 of file fence_inserter.h.
Referenced by col_to_fence(), col_to_var(), compute_fence_options(), mip_fill_matrix(), mip_set_var(), solve(), and var_fence_to_col().
|
protected |
Definition at line 141 of file fence_inserter.h.
Referenced by print_to_file(), print_to_file_2(), print_to_file_3(), print_to_file_4(), and solve().
|
protected |
Definition at line 130 of file fence_inserter.h.
Referenced by mip_set_var().
instrumentert& fence_insertert::instrumenter |
Definition at line 65 of file fence_inserter.h.
Referenced by cycles_visitort::com_constraint(), compute(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), get_type(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), mip_fill_matrix(), mip_set_var(), cycles_visitort::po_edges(), cycles_visitort::porr_constraint(), cycles_visitort::porw_constraint(), cycles_visitort::powr_constraint(), cycles_visitort::poww_constraint(), preprocess(), print_to_file(), print_to_file_2(), print_to_file_3(), print_to_file_4(), print_vars(), fence_user_def_insertert::process_cycles_selection(), fence_assert_insertert::process_cycles_selection(), const_graph_visitort::PT(), and solve().
|
protected |
Definition at line 91 of file fence_inserter.h.
Referenced by mip_fill_matrix(), preprocess(), and print_vars().
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().
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().
const memory_modelt fence_insertert::model |
Definition at line 78 of file fence_inserter.h.
Referenced by compute_fence_options(), mip_fill_matrix(), mip_set_cst(), mip_set_var(), cycles_visitort::po_edges(), and preprocess().
|
protected |
Definition at line 112 of file fence_inserter.h.
Referenced by preprocess().
|
protected |
Definition at line 116 of file fence_inserter.h.
Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().
|
protected |
Definition at line 115 of file fence_inserter.h.
Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().
|
protected |
Definition at line 113 of file fence_inserter.h.
Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().
|
protected |
Definition at line 114 of file fence_inserter.h.
Referenced by mip_fill_matrix(), mip_set_cst(), and preprocess().
|
protected |
Definition at line 84 of file fence_inserter.h.
Referenced by compute(), mip_fill_matrix(), mip_set_var(), and solve().
|
protected |
Definition at line 88 of file fence_inserter.h.
|
protected |
Definition at line 129 of file fence_inserter.h.
Referenced by mip_set_var().