CBMC
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Protected Types | Protected Member Functions | Protected Attributes | List of all members
instrumentert Class Reference

#include <goto2graph.h>

+ Inheritance diagram for instrumentert:
+ Collaboration diagram for instrumentert:

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 (goto_modelt &_goto_model, 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
 
void collect_cycles (memory_modelt model)
 
void collect_cycles_by_SCCs (memory_modelt model)
 Note: can be distributed (#define DISTRIBUTED)
 
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 Member Functions

bool local (const irep_idt &id)
 is local variable?
 
void add_instr_to_interleaving (goto_programt::instructionst::iterator it, goto_programt &interleaving)
 
bool is_cfg_spurious (const event_grapht::critical_cyclet &cyc)
 
unsigned cost (const event_grapht::critical_cyclet::delayt &e)
 cost function
 
void instrument_all_inserter (const set_of_cyclest &set)
 
void instrument_one_event_per_cycle_inserter (const set_of_cyclest &set)
 
void instrument_one_read_per_cycle_inserter (const set_of_cyclest &set)
 
void instrument_one_write_per_cycle_inserter (const set_of_cyclest &set)
 
void instrument_minimum_interference_inserter (const set_of_cyclest &set)
 
void instrument_my_events_inserter (const set_of_cyclest &set, const std::set< event_idt > &events)
 
void print_outputs_local (const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)
 

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
 

Detailed Description

Definition at line 29 of file goto2graph.h.

Member Typedef Documentation

◆ map_function_nodest

typedef std::map<irep_idt, std::pair<std::set<event_idt>, std::set<event_idt> > > instrumentert::map_function_nodest

Definition at line 324 of file goto2graph.h.

◆ set_of_cyclest

typedef std::set<event_grapht::critical_cyclet> instrumentert::set_of_cyclest
protected

Definition at line 60 of file goto2graph.h.

◆ target_sett

typedef std::set<goto_programt::instructiont::targett> instrumentert::target_sett
protected

Definition at line 84 of file goto2graph.h.

Constructor & Destructor Documentation

◆ instrumentert()

instrumentert::instrumentert ( goto_modelt &  _goto_model,
messaget &  _message 
)
inline

Definition at line 357 of file goto2graph.h.

Member Function Documentation

◆ add_instr_to_interleaving()

void instrumentert::add_instr_to_interleaving ( goto_programt::instructionst::iterator  it,
goto_programt &  interleaving 
)
inlineprotected

Definition at line 1226 of file goto2graph.cpp.

◆ cfg_cycles_filter()

void instrumentert::cfg_cycles_filter ( )

Definition at line 1400 of file goto2graph.cpp.

◆ collect_cycles()

void instrumentert::collect_cycles ( memory_modelt  model)
inline

Definition at line 381 of file goto2graph.h.

◆ collect_cycles_by_SCCs()

void instrumentert::collect_cycles_by_SCCs ( memory_modelt  model)

Note: can be distributed (#define DISTRIBUTED)

Definition at line 1608 of file goto2graph.cpp.

◆ cost()

unsigned instrumentert::cost ( const event_grapht::critical_cyclet::delayt &  e)
inlineprotected

cost function

Definition at line 177 of file instrumenter_strategies.cpp.

◆ extract_my_events()

std::set< event_idt > instrumentert::extract_my_events ( )
static

Definition at line 404 of file instrumenter_strategies.cpp.

◆ goto2graph_cfg()

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 88 of file goto2graph.cpp.

◆ instrument_all_inserter()

void instrumentert::instrument_all_inserter ( const set_of_cyclest &  set)
inlineprotected

Definition at line 82 of file instrumenter_strategies.cpp.

◆ instrument_minimum_interference_inserter()

void instrumentert::instrument_minimum_interference_inserter ( const set_of_cyclest &  set)
inlineprotected

Definition at line 192 of file instrumenter_strategies.cpp.

◆ instrument_my_events()

void instrumentert::instrument_my_events ( const std::set< event_idt > &  events)

Definition at line 386 of file instrumenter_strategies.cpp.

◆ instrument_my_events_inserter()

void instrumentert::instrument_my_events_inserter ( const set_of_cyclest &  set,
const std::set< event_idt > &  events 
)
inlineprotected

Definition at line 354 of file instrumenter_strategies.cpp.

◆ instrument_one_event_per_cycle_inserter()

void instrumentert::instrument_one_event_per_cycle_inserter ( const set_of_cyclest &  set)
inlineprotected

Definition at line 111 of file instrumenter_strategies.cpp.

◆ instrument_one_read_per_cycle_inserter()

void instrumentert::instrument_one_read_per_cycle_inserter ( const set_of_cyclest &  set)
inlineprotected

Definition at line 162 of file instrumenter_strategies.cpp.

◆ instrument_one_write_per_cycle_inserter()

void instrumentert::instrument_one_write_per_cycle_inserter ( const set_of_cyclest &  set)
inlineprotected

Definition at line 169 of file instrumenter_strategies.cpp.

◆ instrument_with_strategy()

void instrumentert::instrument_with_strategy ( instrumentation_strategyt  strategy)

Definition at line 23 of file instrumenter_strategies.cpp.

◆ is_cfg_spurious()

bool instrumentert::is_cfg_spurious ( const event_grapht::critical_cyclet &  cyc)
protected

Definition at line 1253 of file goto2graph.cpp.

◆ local()

bool instrumentert::local ( const irep_idt &  id)
inlineprotected

is local variable?

Definition at line 33 of file goto2graph.cpp.

◆ print_map_function_graph()

void instrumentert::print_map_function_graph ( ) const
inline

Definition at line 327 of file goto2graph.h.

◆ print_outputs()

void instrumentert::print_outputs ( memory_modelt  model,
bool  hide_internals 
)

Definition at line 1553 of file goto2graph.cpp.

◆ print_outputs_local()

void instrumentert::print_outputs_local ( const std::set< event_grapht::critical_cyclet > &  set,
std::ofstream &  dot,
std::ofstream &  ref,
std::ofstream &  output,
std::ofstream &  all,
std::ofstream &  table,
memory_modelt  model,
bool  hide_internals 
)
inlineprotected

Definition at line 1447 of file goto2graph.cpp.

◆ set_parameters_collection()

void instrumentert::set_parameters_collection ( unsigned  _max_var = 0,
unsigned  _max_po_trans = 0,
bool  _ignore_arrays = false 
)
inline

Definition at line 394 of file goto2graph.h.

◆ set_rendering_options()

void instrumentert::set_rendering_options ( bool  aligned,
bool  file,
bool  function 
)
inline

Definition at line 414 of file goto2graph.h.

Member Data Documentation

◆ egraph

event_grapht instrumentert::egraph

Definition at line 309 of file goto2graph.h.

◆ egraph_alt

wmm_grapht instrumentert::egraph_alt
protected

Definition at line 40 of file goto2graph.h.

◆ egraph_SCCs

std::vector<std::set<event_idt> > instrumentert::egraph_SCCs

Definition at line 312 of file goto2graph.h.

◆ goto_functions

goto_functionst& instrumentert::goto_functions
protected

Definition at line 36 of file goto2graph.h.

◆ id2cycloc

std::multimap<irep_idt, source_locationt> instrumentert::id2cycloc

Definition at line 355 of file goto2graph.h.

◆ id2loc

std::multimap<irep_idt, source_locationt> instrumentert::id2loc

Definition at line 354 of file goto2graph.h.

◆ map_function_graph

map_function_nodest instrumentert::map_function_graph

Definition at line 325 of file goto2graph.h.

◆ map_vertex_gnode

std::map<event_idt, event_idt> instrumentert::map_vertex_gnode
protected

Definition at line 39 of file goto2graph.h.

◆ message

messaget& instrumentert::message

Definition at line 306 of file goto2graph.h.

◆ ns

namespacet instrumentert::ns

Definition at line 33 of file goto2graph.h.

◆ num_sccs

unsigned instrumentert::num_sccs

Definition at line 319 of file goto2graph.h.

◆ render_by_file

bool instrumentert::render_by_file
protected

Definition at line 46 of file goto2graph.h.

◆ render_by_function

bool instrumentert::render_by_function
protected

Definition at line 47 of file goto2graph.h.

◆ render_po_aligned

bool instrumentert::render_po_aligned
protected

Definition at line 45 of file goto2graph.h.

◆ set_of_cycles

std::set<event_grapht::critical_cyclet> instrumentert::set_of_cycles

Definition at line 315 of file goto2graph.h.

◆ set_of_cycles_per_SCC

std::vector<std::set<event_grapht::critical_cyclet> > instrumentert::set_of_cycles_per_SCC

Definition at line 318 of file goto2graph.h.

◆ unique_id

unsigned instrumentert::unique_id
protected

Definition at line 42 of file goto2graph.h.

◆ var_to_instr

std::set<irep_idt> instrumentert::var_to_instr

Definition at line 353 of file goto2graph.h.

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