cprover
goto2graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrumenter
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
16 
17 #include <map>
18 
19 #include <util/graph.h>
20 #include <util/namespace.h>
21 #include <util/message.h>
22 
24 
25 #include "event_graph.h"
26 #include "wmm.h"
27 
28 class goto_modelt;
29 class value_setst;
30 class local_may_aliast;
31 
33 {
34 public:
35  /* reference to goto-functions and symbol_table */
37 
38 protected:
40 
41  /* alternative representation of graph (SCC) */
42  std::map<event_idt, event_idt> map_vertex_gnode;
44 
45  unsigned unique_id;
46 
47  /* rendering options */
51 
52  bool inline local(const irep_idt &id);
53 
54  void inline add_instr_to_interleaving(
55  goto_programt::instructionst::iterator it,
56  goto_programt &interleaving);
57 
58  /* deprecated */
60 
62 
63  typedef std::set<event_grapht::critical_cyclet> set_of_cyclest;
64  void inline instrument_all_inserter(
65  const set_of_cyclest &set);
67  const set_of_cyclest &set);
69  const set_of_cyclest &set);
71  const set_of_cyclest &set);
73  const set_of_cyclest &set);
75  const set_of_cyclest &set, const std::set<event_idt> &events);
76 
77  void inline print_outputs_local(
78  const std::set<event_grapht::critical_cyclet> &set,
79  std::ofstream &dot,
80  std::ofstream &ref,
81  std::ofstream &output,
82  std::ofstream &all,
83  std::ofstream &table,
84  memory_modelt model,
85  bool hide_internals);
86 
87  typedef std::set<goto_programt::instructiont::targett> target_sett;
88 
90  {
91  protected:
94 
95  /* pointer to the egraph(s) that we construct */
97  std::vector<std::set<event_idt>> &egraph_SCCs;
99 
100  /* for thread marking (dynamic) */
101  unsigned current_thread;
102  unsigned coming_from;
103 
107  value_setst &value_sets
108  #ifdef LOCAL_MAY
109  , local_may_aliast local_may
110  #endif
111  ) const; // NOLINT(whitespace/parens)
112 
113  /* transformers */
114  void visit_cfg_thread() const;
115  void visit_cfg_propagate(goto_programt::instructionst::iterator i_it);
116  void visit_cfg_body(
118  loop_strategyt replicate_body,
119  value_setst &value_sets
120  #ifdef LOCAL_MAY
121  , local_may_aliast &local_may
122  #endif
123  ); // deprecated NOLINT(whitespace/parens)
128  void visit_cfg_assign(
129  value_setst &value_sets,
130  goto_programt::instructionst::iterator &i_it,
131  bool no_dependencies
132 #ifdef LOCAL_MAY
133  ,
134  local_may_aliast &local_may
135 #endif
136  ); // NOLINT(whitespace/parens)
137  void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
138  void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
139  void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it);
140  void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it);
141  void visit_cfg_function_call(value_setst &value_sets,
142  goto_programt::instructionst::iterator i_it,
143  memory_modelt model,
144  bool no_dependenciess,
145  loop_strategyt duplicate_body);
146  void visit_cfg_goto(
147  goto_programt::instructionst::iterator i_it,
148  /* forces the duplication of all the loops, with array or not
149  otherwise, duplication of loops with array accesses only */
150  loop_strategyt replicate_body,
151  value_setst &value_sets
152  #ifdef LOCAL_MAY
153  , local_may_aliast &local_may
154  #endif
155  ); // NOLINT(whitespace/parens)
156  void visit_cfg_reference_function(irep_idt id_function);
157 
158  public:
159  virtual ~cfg_visitort()
160  {
161  }
162 
163  unsigned max_thread;
164 
165  /* relations between irep and Reads/Writes */
166  typedef std::multimap<irep_idt, event_idt> id2nodet;
167  typedef std::pair<irep_idt, event_idt> id2node_pairt;
169 
170  unsigned write_counter;
171  unsigned read_counter;
172  unsigned ws_counter;
173  unsigned fr_rf_counter;
174 
175  /* previous nodes (fwd analysis) */
176  typedef std::pair<event_idt, event_idt> nodet;
177  typedef std::map<goto_programt::const_targett, std::set<nodet> >
179 
181  std::set<goto_programt::const_targett> updated;
182 
183  /* "next nodes" (bwd steps in fwd/bck analysis) */
185 
186  #define add_all_pos(it, target, source) \
187  for(std::set<nodet>::const_iterator \
188  it=(source).begin(); \
189  it!=(source).end(); ++it) \
190  (target).insert(*it);
191 
192  #ifdef CONTEXT_INSENSITIVE
193  /* to keep track of the functions (and their start/end nodes) */
194  std::stack<irep_idt> stack_fun;
195  irep_idt cur_fun;
196  std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
197  #endif
198 
199  /* current thread number */
200  unsigned thread;
201 
202  /* dependencies */
204 
205  /* writes and reads to unknown addresses -- conservative */
206  std::set<event_idt> unknown_read_nodes;
207  std::set<event_idt> unknown_write_nodes;
208 
209  /* set of functions visited so far -- we don't handle recursive functions */
210  std::set<irep_idt> functions_met;
211 
212  cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
213  :ns(_ns), instrumenter(_instrumenter), egraph(_instrumenter.egraph),
214  egraph_SCCs(_instrumenter.egraph_SCCs),
215  egraph_alt(_instrumenter.egraph_alt)
216  {
217  write_counter = 0;
218  read_counter = 0;
219  ws_counter = 0;
220  fr_rf_counter = 0;
221  thread = 0;
222  current_thread = 0;
223  max_thread = 0;
224  coming_from = 0;
225  }
226 
227  void inline enter_function(const irep_idt &function)
228  {
229  if(functions_met.find(function)!=functions_met.end())
230  throw "sorry, doesn't handle recursive function for the moment";
231  functions_met.insert(function);
232  }
233 
234  void inline leave_function(const irep_idt &function)
235  {
236  functions_met.erase(function);
237  }
238 
239  void inline visit_cfg(
240  value_setst &value_sets,
241  memory_modelt model,
242  bool no_dependencies,
243  loop_strategyt duplicate_body,
244  const irep_idt &function)
245  {
246  /* ignore recursive calls -- underapproximation */
247  try
248  {
249  /* forbids recursive function */
250  enter_function(function);
251  std::set<nodet> end_out;
252  visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
253  function, end_out);
254  leave_function(function);
255  }
256  catch(const std::string &s)
257  {
259  }
260  }
261 
270  virtual void visit_cfg_function(
271  value_setst &value_sets,
272  memory_modelt model,
273  bool no_dependencies,
274  loop_strategyt duplicate_body,
275  const irep_idt &function,
276  std::set<nodet> &ending_vertex);
277 
278  bool inline local(const irep_idt &i);
279  };
280 
281 public:
282  /* message */
284 
285  /* graph */
287 
288  /* graph split into strongly connected components */
289  std::vector<std::set<event_idt> > egraph_SCCs;
290 
291  /* critical cycles */
292  std::set<event_grapht::critical_cyclet> set_of_cycles;
293 
294  /* critical cycles per SCC */
295  std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
296  unsigned num_sccs;
297 
298  /* map from function to begin and end of the corresponding part of the
299  graph */
300  typedef std::map<irep_idt, std::pair<std::set<event_idt>,
301  std::set<event_idt> > > map_function_nodest;
303 
305  {
306  for(map_function_nodest::const_iterator it=map_function_graph.begin();
307  it!=map_function_graph.end();
308  ++it)
309  {
310  message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
311  message.debug() << "Start nodes: ";
312  for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
313  in_it!=it->second.first.end();
314  ++in_it)
315  message.debug() << *in_it << " ";
317  message.debug() << "End nodes: ";
318  for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
319  in_it!=it->second.second.end();
320  ++in_it)
321  message.debug() << *in_it << " ";
323  }
324  }
325 
326  /* variables to instrument, locations of variables to instrument on
327  the cycles, and locations of all the variables on the critical cycles */
328  /* TODO: those maps are here to interface easily with weak_mem.cpp,
329  but a rewriting of weak_mem can eliminate them */
330  std::set<irep_idt> var_to_instr;
331  std::multimap<irep_idt, source_locationt> id2loc;
332  std::multimap<irep_idt, source_locationt> id2cycloc;
333 
335  goto_modelt &_goto_model,
336  messaget &_message):
337  ns(_goto_model.symbol_table),
338  goto_functions(_goto_model.goto_functions),
339  render_po_aligned(true),
340  render_by_file(false),
341  render_by_function(false),
342  message(_message),
343  egraph(_message),
344  num_sccs(0)
345  {
346  }
347 
348  /* abstracts goto-programs in abstract event graph, and computes
349  the thread numbering and returns the max number */
350  unsigned goto2graph_cfg(
351  value_setst &value_sets,
352  memory_modelt model,
353  bool no_dependencies,
354  /* forces the duplication, with arrays or not; otherwise, arrays only */
355  loop_strategyt duplicate_body);
356 
357  /* collects directly all the cycles in the graph */
359  {
361  num_sccs = 0;
362  }
363 
364  /* collects the cycles in the graph by SCCs */
366 
367  /* filters cycles spurious by CFG */
368  void cfg_cycles_filter();
369 
370  /* sets parameters for collection, if required */
372  unsigned _max_var = 0,
373  unsigned _max_po_trans = 0,
374  bool _ignore_arrays = false)
375  {
376  egraph.set_parameters_collection(_max_var, _max_po_trans, _ignore_arrays);
377  }
378 
379  /* builds the relations between unsafe pairs in the critical cycles and
380  instructions to instrument in the code */
381 
382  /* strategies for instrumentation */
384  void instrument_my_events(const std::set<event_idt> &events);
385 
386  /* retrieves events to filter in the instrumentation choice
387  with option --my-events */
388  static std::set<event_idt> extract_my_events();
389 
390  /* sets rendering options */
391  void set_rendering_options(bool aligned, bool file, bool function)
392  {
393  render_po_aligned = aligned;
395  render_by_function = function;
396  assert(!render_by_file || !render_by_function);
397  }
398 
399  /* prints outputs:
400  - cycles.dot: graph of the instrumented cycles
401  - ref.txt: names of the instrumented cycles
402  - output.txt: names of the instructions in the code
403  - all.txt: all */
404  void print_outputs(memory_modelt model, bool hide_internals);
405 };
406 
407 #endif // CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
instrumentert::egraph_SCCs
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:289
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
instrumentert::print_map_function_graph
void print_map_function_graph() const
Definition: goto2graph.h:304
instrumentert::collect_cycles
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:358
instrumentert::egraph_alt
wmm_grapht egraph_alt
Definition: goto2graph.h:43
instrumentert::set_of_cycles_per_SCC
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:295
instrumentert::cfg_visitort::thread
unsigned thread
Definition: goto2graph.h:200
instrumentert::cfg_visitort::visit_cfg_backedge
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:556
instrumentert::cfg_visitort::current_thread
unsigned current_thread
Definition: goto2graph.h:101
instrumentert::instrument_my_events_inserter
void instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)
Definition: instrumenter_strategies.cpp:355
instrumentert::cfg_visitort::contains_shared_array
bool contains_shared_array(goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
Definition: goto2graph.cpp:398
instrumentert::cfg_visitort::visit_cfg_asm_fence
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:745
instrumentert::cfg_visitort::enter_function
void enter_function(const irep_idt &function)
Definition: goto2graph.h:227
instrumentert::cfg_visitort::fr_rf_counter
unsigned fr_rf_counter
Definition: goto2graph.h:173
instrumentert::instrument_my_events
void instrument_my_events(const std::set< event_idt > &events)
Definition: instrumenter_strategies.cpp:387
instrumentert::print_outputs
void print_outputs(memory_modelt model, bool hide_internals)
Definition: goto2graph.cpp:1468
instrumentert::set_parameters_collection
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:371
dot
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:352
event_graph.h
grapht< abstract_eventt >
file
Definition: kdev_t.h:19
instrumentert::cfg_visitort::visit_cfg_function
virtual void visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
Definition: goto2graph.cpp:147
goto_model.h
instrumentert::target_sett
std::set< goto_programt::instructiont::targett > target_sett
Definition: goto2graph.h:87
instrumentert::cfg_visitort::egraph_SCCs
std::vector< std::set< event_idt > > & egraph_SCCs
Definition: goto2graph.h:97
instrumentert::cfg_visitort::visit_cfg_duplicate
void visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it)
Definition: goto2graph.cpp:492
goto_modelt
Definition: goto_model.h:24
instrumentert::cfg_visitort
Definition: goto2graph.h:89
instrumentert::map_function_nodest
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition: goto2graph.h:301
messaget::eom
static eomt eom
Definition: message.h:284
instrumentert::num_sccs
unsigned num_sccs
Definition: goto2graph.h:296
instrumentert::cfg_visitort::visit_cfg_reference_function
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
Definition: goto2graph.cpp:306
instrumentert::cfg_visitort::incoming_post
std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
Definition: goto2graph.h:178
namespace.h
instrumentert::cfg_visitort::id2node_pairt
std::pair< irep_idt, event_idt > id2node_pairt
Definition: goto2graph.h:167
loop_strategyt
loop_strategyt
Definition: wmm.h:36
instrumentert::render_po_aligned
bool render_po_aligned
Definition: goto2graph.h:48
instrumentert::cfg_visitort::visit_cfg_thread
void visit_cfg_thread() const
Definition: goto2graph.cpp:296
local_may_aliast
Definition: local_may_alias.h:25
instrumentert::goto2graph_cfg
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 f...
Definition: goto2graph.cpp:87
instrumentert::id2loc
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:331
instrumentert::id2cycloc
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:332
instrumentert::ns
namespacet ns
Definition: goto2graph.h:36
instrumentert::cfg_visitort::updated
std::set< goto_programt::const_targett > updated
Definition: goto2graph.h:181
instrumentert::set_of_cyclest
std::set< event_grapht::critical_cyclet > set_of_cyclest
Definition: goto2graph.h:63
instrumentert::cfg_visitort::visit_cfg_goto
void visit_cfg_goto(goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
Definition: goto2graph.cpp:622
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
instrumentert::unique_id
unsigned unique_id
Definition: goto2graph.h:45
instrumentert::cfg_visitort::unknown_write_nodes
std::set< event_idt > unknown_write_nodes
Definition: goto2graph.h:207
instrumentert::instrument_one_write_per_cycle_inserter
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
Definition: instrumenter_strategies.cpp:170
event_grapht::critical_cyclet::delayt
Definition: event_graph.h:164
instrumentert::collect_cycles_by_SCCs
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
Definition: goto2graph.cpp:1523
instrumentert::set_rendering_options
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:391
instrumentert::cfg_visitort::out_pos
incoming_post out_pos
Definition: goto2graph.h:184
instrumentert::instrument_one_event_per_cycle_inserter
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
Definition: instrumenter_strategies.cpp:112
instrumentert::cfg_visitort::map_reads
id2nodet map_reads
Definition: goto2graph.h:168
instrumentert::render_by_function
bool render_by_function
Definition: goto2graph.h:50
event_grapht::collect_cycles
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Definition: event_graph.h:552
instrumentert::cfg_visitort::leave_function
void leave_function(const irep_idt &function)
Definition: goto2graph.h:234
instrumentert::cfg_visitort::~cfg_visitort
virtual ~cfg_visitort()
Definition: goto2graph.h:159
instrumentert::cost
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
Definition: instrumenter_strategies.cpp:178
instrumentert::cfg_visitort::visit_cfg_assign
void visit_cfg_assign(value_setst &value_sets, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
Definition: goto2graph.cpp:785
instrumentert::cfg_visitort::coming_from
unsigned coming_from
Definition: goto2graph.h:102
instrumentert::cfg_visitort::max_thread
unsigned max_thread
Definition: goto2graph.h:163
instrumentert::local
bool local(const irep_idt &id)
is local variable?
Definition: goto2graph.cpp:32
instrumentert::cfg_visitort::in_pos
incoming_post in_pos
Definition: goto2graph.h:180
instrumentert::map_function_graph
map_function_nodest map_function_graph
Definition: goto2graph.h:302
instrumentert::cfg_visitort::instrumenter
instrumentert & instrumenter
Definition: goto2graph.h:93
instrumentert::cfg_visitort::ns
namespacet & ns
Definition: goto2graph.h:92
instrumentert::cfg_visitort::ws_counter
unsigned ws_counter
Definition: goto2graph.h:172
instrumentert::cfg_visitort::visit_cfg_lwfence
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:713
instrumentert::cfg_visitort::visit_cfg
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function)
Definition: goto2graph.h:239
instrumentert::instrumentert
instrumentert(goto_modelt &_goto_model, messaget &_message)
Definition: goto2graph.h:334
instrumentert::cfg_visitort::egraph_alt
wmm_grapht & egraph_alt
Definition: goto2graph.h:98
instrumentert::is_cfg_spurious
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
Definition: goto2graph.cpp:1174
memory_modelt
memory_modelt
Definition: wmm.h:17
instrumentert::cfg_visitort::map_writes
id2nodet map_writes
Definition: goto2graph.h:168
instrumentert
Definition: goto2graph.h:32
instrumentert::egraph
event_grapht egraph
Definition: goto2graph.h:286
instrumentert::add_instr_to_interleaving
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
Definition: goto2graph.cpp:1142
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
value_setst
Definition: value_sets.h:21
instrumentert::instrument_with_strategy
void instrument_with_strategy(instrumentation_strategyt strategy)
Definition: instrumenter_strategies.cpp:24
graph.h
instrumentert::map_vertex_gnode
std::map< event_idt, event_idt > map_vertex_gnode
Definition: goto2graph.h:42
instrumentert::cfg_visitort::visit_cfg_body
void visit_cfg_body(goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:447
instrumentert::instrument_minimum_interference_inserter
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
Definition: instrumenter_strategies.cpp:193
instrumentert::render_by_file
bool render_by_file
Definition: goto2graph.h:49
event_grapht::set_parameters_collection
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: event_graph.h:567
instrumentert::message
messaget & message
Definition: goto2graph.h:283
event_grapht
Definition: event_graph.h:35
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
instrumentert::cfg_visitort::nodet
std::pair< event_idt, event_idt > nodet
Definition: goto2graph.h:176
instrumentert::cfg_visitort::data_dp
data_dpt data_dp
Definition: goto2graph.h:203
data_dpt
Definition: data_dp.h:51
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
instrumentation_strategyt
instrumentation_strategyt
Definition: wmm.h:26
instrumentert::instrument_all_inserter
void instrument_all_inserter(const set_of_cyclest &set)
Definition: instrumenter_strategies.cpp:83
messaget::debug
mstreamt & debug() const
Definition: message.h:416
instrumentert::extract_my_events
static std::set< event_idt > extract_my_events()
Definition: instrumenter_strategies.cpp:405
instrumentert::cfg_visitort::functions_met
std::set< irep_idt > functions_met
Definition: goto2graph.h:210
wmm.h
event_grapht::critical_cyclet
Definition: event_graph.h:39
message.h
instrumentert::cfg_visitort::visit_cfg_propagate
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:284
all
Definition: wmm.h:28
instrumentert::cfg_visitort::egraph
event_grapht & egraph
Definition: goto2graph.h:96
messaget::warning
mstreamt & warning() const
Definition: message.h:391
instrumentert::cfg_cycles_filter
void cfg_cycles_filter()
Definition: goto2graph.cpp:1315
instrumentert::print_outputs_local
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)
Definition: goto2graph.cpp:1362
instrumentert::instrument_one_read_per_cycle_inserter
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
Definition: instrumenter_strategies.cpp:163
instrumentert::cfg_visitort::visit_cfg_fence
void visit_cfg_fence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:1101
instrumentert::cfg_visitort::cfg_visitort
cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
Definition: goto2graph.h:212
instrumentert::var_to_instr
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:330
instrumentert::cfg_visitort::write_counter
unsigned write_counter
Definition: goto2graph.h:170
instrumentert::goto_functions
goto_functionst & goto_functions
Definition: goto2graph.h:39
instrumentert::set_of_cycles
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:292
instrumentert::cfg_visitort::local
bool local(const irep_idt &i)
Definition: goto2graph.cpp:80
instrumentert::cfg_visitort::visit_cfg_function_call
void visit_cfg_function_call(value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body)
Definition: goto2graph.cpp:651
instrumentert::cfg_visitort::id2nodet
std::multimap< irep_idt, event_idt > id2nodet
Definition: goto2graph.h:166
instrumentert::cfg_visitort::unknown_read_nodes
std::set< event_idt > unknown_read_nodes
Definition: goto2graph.h:206
instrumentert::cfg_visitort::read_counter
unsigned read_counter
Definition: goto2graph.h:171
instrumentert::cfg_visitort::visit_cfg_skip
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:1136