cprover
|
#include <goto2graph.h>
Classes | |
class | cfg_visitort |
Public Types | |
typedef std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > | map_function_nodest |
Public Member Functions | |
void | print_map_function_graph () const |
instrumentert (symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &_message) | |
unsigned | goto2graph_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body) |
goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions More... | |
void | collect_cycles (memory_modelt model) |
void | collect_cycles_by_SCCs (memory_modelt model) |
Note: can be distributed (#define DISTRIBUTED) More... | |
void | cfg_cycles_filter () |
void | set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false) |
void | instrument_with_strategy (instrumentation_strategyt strategy) |
void | instrument_my_events (const std::set< event_idt > &events) |
void | set_rendering_options (bool aligned, bool file, bool function) |
void | print_outputs (memory_modelt model, bool hide_internals) |
Static Public Member Functions | |
static std::set< event_idt > | extract_my_events () |
Public Attributes | |
namespacet | ns |
messaget & | message |
event_grapht | egraph |
std::vector< std::set< event_idt > > | egraph_SCCs |
std::set< event_grapht::critical_cyclet > | set_of_cycles |
std::vector< std::set< event_grapht::critical_cyclet > > | set_of_cycles_per_SCC |
unsigned | num_sccs |
map_function_nodest | map_function_graph |
std::set< irep_idt > | var_to_instr |
std::multimap< irep_idt, source_locationt > | id2loc |
std::multimap< irep_idt, source_locationt > | id2cycloc |
Protected Types | |
typedef std::set< event_grapht::critical_cyclet > | set_of_cyclest |
typedef std::set< goto_programt::instructiont::targett > | target_sett |
Protected Attributes | |
goto_functionst & | goto_functions |
std::map< event_idt, event_idt > | map_vertex_gnode |
wmm_grapht | egraph_alt |
unsigned | unique_id |
bool | render_po_aligned |
bool | render_by_file |
bool | render_by_function |
Definition at line 33 of file goto2graph.h.
typedef std::map<irep_idt, std::pair<std::set<event_idt>, std::set<event_idt> > > instrumentert::map_function_nodest |
Definition at line 298 of file goto2graph.h.
|
protected |
Definition at line 64 of file goto2graph.h.
|
protected |
Definition at line 88 of file goto2graph.h.
|
inline |
Definition at line 331 of file goto2graph.h.
|
inlineprotected |
Definition at line 1155 of file goto2graph.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction().
Referenced by is_cfg_spurious().
void instrumentert::cfg_cycles_filter | ( | ) |
Definition at line 1328 of file goto2graph.cpp.
References messaget::eom(), is_cfg_spurious(), message, num_sccs, set_of_cycles, set_of_cycles_per_SCC, and messaget::status().
Referenced by fence_weak_memory(), and weak_memory().
|
inline |
Definition at line 349 of file goto2graph.h.
References event_grapht::collect_cycles(), egraph, num_sccs, and set_of_cycles.
Referenced by fence_weak_memory(), and weak_memory().
void instrumentert::collect_cycles_by_SCCs | ( | memory_modelt | model | ) |
Note: can be distributed (#define DISTRIBUTED)
Definition at line 1536 of file goto2graph.cpp.
References event_grapht::collect_cycles(), egraph, egraph_SCCs, num_sccs, and set_of_cycles_per_SCC.
Referenced by fence_weak_memory(), and weak_memory().
|
inlineprotected |
cost function
Definition at line 177 of file instrumenter_strategies.cpp.
References egraph, event_grapht::critical_cyclet::delayt::first, event_grapht::critical_cyclet::delayt::is_po, event_grapht::critical_cyclet::delayt::second, and abstract_eventt::Write.
Referenced by instrument_minimum_interference_inserter().
|
static |
Definition at line 406 of file instrumenter_strategies.cpp.
Referenced by weak_memory().
unsigned instrumentert::goto2graph_cfg | ( | value_setst & | value_sets, |
memory_modelt | model, | ||
bool | no_dependencies, | ||
loop_strategyt | duplicate_body | ||
) |
goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions
Definition at line 93 of file goto2graph.cpp.
References egraph_alt, egraph_SCCs, goto_functions_templatet< bodyT >::entry_point(), messaget::eom(), instrumentert::cfg_visitort::fr_rf_counter, goto_functions_templatet< bodyT >::function_map, goto_functions, map_vertex_gnode, instrumentert::cfg_visitort::max_thread, message, ns, num_sccs, instrumentert::cfg_visitort::read_counter, grapht< N >::SCCs(), grapht< N >::size(), messaget::statistics(), messaget::status(), instrumentert::cfg_visitort::visit_cfg(), instrumentert::cfg_visitort::write_counter, and instrumentert::cfg_visitort::ws_counter.
Referenced by fence_pensieve(), fence_weak_memory(), and weak_memory().
|
inlineprotected |
Definition at line 83 of file instrumenter_strategies.cpp.
References egraph, id2loc, set_of_cycles, abstract_eventt::source_location, var_to_instr, and abstract_eventt::variable.
Referenced by instrument_with_strategy().
|
inlineprotected |
Definition at line 192 of file instrumenter_strategies.cpp.
References cost(), messaget::debug(), egraph, messaget::eom(), id2loc, message, set_of_cycles, abstract_eventt::source_location, messaget::statistics(), var_to_instr, and abstract_eventt::variable.
Referenced by instrument_with_strategy().
void instrumentert::instrument_my_events | ( | const std::set< event_idt > & | events | ) |
Definition at line 388 of file instrumenter_strategies.cpp.
References messaget::debug(), messaget::eom(), id2cycloc, id2loc, instrument_my_events_inserter(), message, my_events, num_sccs, set_of_cycles, set_of_cycles_per_SCC, and var_to_instr.
Referenced by weak_memory().
|
inlineprotected |
Definition at line 356 of file instrumenter_strategies.cpp.
References egraph, id2loc, my_events, abstract_eventt::source_location, var_to_instr, and abstract_eventt::variable.
Referenced by instrument_my_events().
|
inlineprotected |
Definition at line 111 of file instrumenter_strategies.cpp.
References egraph, id2loc, set_of_cycles, abstract_eventt::source_location, var_to_instr, and abstract_eventt::variable.
Referenced by instrument_with_strategy().
|
inlineprotected |
Definition at line 162 of file instrumenter_strategies.cpp.
Referenced by instrument_with_strategy().
|
inlineprotected |
Definition at line 169 of file instrumenter_strategies.cpp.
Referenced by instrument_with_strategy().
void instrumentert::instrument_with_strategy | ( | instrumentation_strategyt | strategy | ) |
Definition at line 24 of file instrumenter_strategies.cpp.
References all, messaget::debug(), messaget::eom(), id2cycloc, id2loc, instrument_all_inserter(), instrument_minimum_interference_inserter(), instrument_one_event_per_cycle_inserter(), instrument_one_read_per_cycle_inserter(), instrument_one_write_per_cycle_inserter(), message, min_interference, my_events, num_sccs, one_event_per_cycle, read_first, set_of_cycles, set_of_cycles_per_SCC, var_to_instr, and write_first.
Referenced by weak_memory().
|
protected |
Definition at line 1187 of file goto2graph.cpp.
References add_instr_to_interleaving(), goto_function_templatet< bodyT >::body, goto_program_templatet< codeT, guardT >::copy_from(), messaget::debug(), egraph, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), Forall_goto_functions, forall_goto_program_instructions, Forall_goto_program_instructions, goto_functions_templatet< bodyT >::function_map, goto_functions, goto_program_templatet< codeT, guardT >::instructions, message, event_grapht::po_out(), bmct::run(), and abstract_eventt::source_location.
Referenced by cfg_cycles_filter().
|
inlineprotected |
is local variable?
Definition at line 38 of file goto2graph.cpp.
References CPROVER_PREFIX, messaget::debug(), messaget::eom(), has_prefix(), id2string(), symbolt::is_static_lifetime, symbolt::is_thread_local, namespacet::lookup(), message, ns, and pos().
Referenced by instrumentert::cfg_visitort::local(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
inline |
Definition at line 301 of file goto2graph.h.
References messaget::debug(), messaget::eom(), map_function_graph, and message.
Referenced by fence_weak_memory().
void instrumentert::print_outputs | ( | memory_modelt | model, |
bool | hide_internals | ||
) |
Definition at line 1481 of file goto2graph.cpp.
References all, messaget::debug(), dot(), messaget::eom(), message, num_sccs, print_outputs_local(), set_of_cycles, and set_of_cycles_per_SCC.
Referenced by fence_weak_memory(), and weak_memory().
|
inlineprotected |
Definition at line 1375 of file goto2graph.cpp.
References all, messaget::debug(), dot(), egraph, messaget::eom(), source_locationt::get_file(), source_locationt::get_function(), abstract_eventt::get_operation(), abstract_eventt::id, id2loc, message, render_by_file, render_by_function, render_po_aligned, abstract_eventt::source_location, abstract_eventt::thread, var_to_instr, and abstract_eventt::variable.
Referenced by print_outputs().
|
inline |
Definition at line 362 of file goto2graph.h.
References egraph, and event_grapht::set_parameters_collection().
Referenced by fence_pensieve(), fence_weak_memory(), and weak_memory().
|
inline |
Definition at line 382 of file goto2graph.h.
References render_by_file, render_by_function, and render_po_aligned.
Referenced by fence_weak_memory(), and weak_memory().
event_grapht instrumentert::egraph |
Definition at line 283 of file goto2graph.h.
Referenced by collect_cycles(), collect_cycles_by_SCCs(), instrumenter_pensievet::collect_pairs(), instrumenter_pensievet::collect_pairs_naive(), cycles_visitort::com_constraint(), cost(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), fence_weak_memory(), instrument_all_inserter(), instrument_minimum_interference_inserter(), instrument_my_events_inserter(), instrument_one_event_per_cycle_inserter(), is_cfg_spurious(), cycles_visitort::po_edges(), cycles_visitort::porr_constraint(), cycles_visitort::porw_constraint(), cycles_visitort::powr_constraint(), cycles_visitort::poww_constraint(), print_outputs_local(), fence_insertert::print_to_file(), fence_insertert::print_to_file_2(), fence_insertert::print_to_file_3(), fence_insertert::print_to_file_4(), const_graph_visitort::PT(), set_parameters_collection(), fence_insertert::solve(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_backedge(), instrumentert::cfg_visitort::visit_cfg_duplicate(), instrumentert::cfg_visitort::visit_cfg_fence(), instrumentert::cfg_visitort::visit_cfg_function(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
|
protected |
Definition at line 44 of file goto2graph.h.
Referenced by goto2graph_cfg(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_backedge(), instrumentert::cfg_visitort::visit_cfg_duplicate(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
std::vector<std::set<event_idt> > instrumentert::egraph_SCCs |
Definition at line 286 of file goto2graph.h.
Referenced by collect_cycles_by_SCCs(), fence_weak_memory(), goto2graph_cfg(), and weak_memory().
|
protected |
Definition at line 40 of file goto2graph.h.
Referenced by goto2graph_cfg(), and is_cfg_spurious().
std::multimap<irep_idt, source_locationt> instrumentert::id2cycloc |
Definition at line 329 of file goto2graph.h.
Referenced by instrument_my_events(), instrument_with_strategy(), and weak_memory().
std::multimap<irep_idt, source_locationt> instrumentert::id2loc |
Definition at line 328 of file goto2graph.h.
Referenced by instrument_all_inserter(), instrument_minimum_interference_inserter(), instrument_my_events(), instrument_my_events_inserter(), instrument_one_event_per_cycle_inserter(), instrument_with_strategy(), print_outputs_local(), and weak_memory().
map_function_nodest instrumentert::map_function_graph |
Definition at line 299 of file goto2graph.h.
Referenced by print_map_function_graph().
Definition at line 43 of file goto2graph.h.
Referenced by goto2graph_cfg().
messaget& instrumentert::message |
Definition at line 280 of file goto2graph.h.
Referenced by cfg_cycles_filter(), fence_insertert::compute(), fence_insertert::get_type(), goto2graph_cfg(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), instrument_minimum_interference_inserter(), instrument_my_events(), instrument_with_strategy(), is_cfg_spurious(), local(), fence_insertert::mip_fill_matrix(), fence_insertert::preprocess(), print_map_function_graph(), print_outputs(), print_outputs_local(), fence_insertert::print_to_file_3(), fence_insertert::print_to_file_4(), fence_insertert::print_vars(), fence_insertert::solve(), and instrumentert::cfg_visitort::visit_cfg().
namespacet instrumentert::ns |
Definition at line 37 of file goto2graph.h.
Referenced by instrumenter_pensievet::collect_pairs(), instrumenter_pensievet::collect_pairs_naive(), instrumentert::cfg_visitort::contains_shared_array(), fence_insertert::get_type(), goto2graph_cfg(), local(), instrumentert::cfg_visitort::visit_cfg_assign(), and instrumentert::cfg_visitort::visit_cfg_function().
unsigned instrumentert::num_sccs |
Definition at line 293 of file goto2graph.h.
Referenced by cfg_cycles_filter(), collect_cycles(), collect_cycles_by_SCCs(), fence_weak_memory(), goto2graph_cfg(), instrument_my_events(), instrument_with_strategy(), print_outputs(), and weak_memory().
|
protected |
Definition at line 50 of file goto2graph.h.
Referenced by print_outputs_local(), and set_rendering_options().
|
protected |
Definition at line 51 of file goto2graph.h.
Referenced by print_outputs_local(), and set_rendering_options().
|
protected |
Definition at line 49 of file goto2graph.h.
Referenced by print_outputs_local(), and set_rendering_options().
std::set<event_grapht::critical_cyclet> instrumentert::set_of_cycles |
Definition at line 289 of file goto2graph.h.
Referenced by cfg_cycles_filter(), collect_cycles(), fence_weak_memory(), instrument_all_inserter(), instrument_minimum_interference_inserter(), instrument_my_events(), instrument_one_event_per_cycle_inserter(), instrument_with_strategy(), fence_insertert::mip_set_var(), cycles_visitort::po_edges(), fence_insertert::preprocess(), print_outputs(), fence_user_def_insertert::process_cycles_selection(), fence_assert_insertert::process_cycles_selection(), fence_insertert::solve(), and weak_memory().
std::vector<std::set<event_grapht::critical_cyclet> > instrumentert::set_of_cycles_per_SCC |
Definition at line 292 of file goto2graph.h.
Referenced by cfg_cycles_filter(), collect_cycles_by_SCCs(), fence_weak_memory(), instrument_my_events(), instrument_with_strategy(), print_outputs(), and weak_memory().
|
protected |
Definition at line 46 of file goto2graph.h.
std::set<irep_idt> instrumentert::var_to_instr |
Definition at line 327 of file goto2graph.h.
Referenced by instrument_all_inserter(), instrument_minimum_interference_inserter(), instrument_my_events(), instrument_my_events_inserter(), instrument_one_event_per_cycle_inserter(), instrument_with_strategy(), print_outputs_local(), and weak_memory().