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 
105  const irep_idt &function_id,
108  value_setst &value_sets
109 #ifdef LOCAL_MAY
110  ,
111  local_may_aliast local_may
112 #endif
113  ) const; // NOLINT(whitespace/parens)
114 
115  /* transformers */
116  void visit_cfg_thread() const;
117  void visit_cfg_propagate(goto_programt::instructionst::iterator i_it);
118  void visit_cfg_body(
119  const irep_idt &function_id,
120  const goto_programt &goto_program,
122  loop_strategyt replicate_body,
123  value_setst &value_sets
124 #ifdef LOCAL_MAY
125  ,
126  local_may_aliast &local_may
127 #endif
128  ); // deprecated NOLINT(whitespace/parens)
131  void inline visit_cfg_duplicate(
132  const goto_programt &goto_program,
135  void visit_cfg_assign(
136  value_setst &value_sets,
137  const irep_idt &function_id,
138  goto_programt::instructionst::iterator &i_it,
139  bool no_dependencies
140 #ifdef LOCAL_MAY
141  ,
142  local_may_aliast &local_may
143 #endif
144  ); // NOLINT(whitespace/parens)
145  void visit_cfg_fence(
146  goto_programt::instructionst::iterator i_it,
147  const irep_idt &function_id);
148  void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
149  void visit_cfg_lwfence(
150  goto_programt::instructionst::iterator i_it,
151  const irep_idt &function_id);
152  void visit_cfg_asm_fence(
153  goto_programt::instructionst::iterator i_it,
154  const irep_idt &function_id);
155  void visit_cfg_function_call(value_setst &value_sets,
156  goto_programt::instructionst::iterator i_it,
157  memory_modelt model,
158  bool no_dependenciess,
159  loop_strategyt duplicate_body);
160  void visit_cfg_goto(
161  const irep_idt &function_id,
162  const goto_programt &goto_program,
163  goto_programt::instructionst::iterator i_it,
164  /* forces the duplication of all the loops, with array or not
165  otherwise, duplication of loops with array accesses only */
166  loop_strategyt replicate_body,
167  value_setst &value_sets
168 #ifdef LOCAL_MAY
169  ,
170  local_may_aliast &local_may
171 #endif
172  ); // NOLINT(whitespace/parens)
173  void visit_cfg_reference_function(irep_idt id_function);
174 
175  public:
176  virtual ~cfg_visitort()
177  {
178  }
179 
180  unsigned max_thread;
181 
182  /* relations between irep and Reads/Writes */
183  typedef std::multimap<irep_idt, event_idt> id2nodet;
184  typedef std::pair<irep_idt, event_idt> id2node_pairt;
186 
187  unsigned write_counter;
188  unsigned read_counter;
189  unsigned ws_counter;
190  unsigned fr_rf_counter;
191 
192  /* previous nodes (fwd analysis) */
193  typedef std::pair<event_idt, event_idt> nodet;
194  typedef std::map<goto_programt::const_targett, std::set<nodet> >
196 
198  std::set<goto_programt::const_targett> updated;
199 
200  /* "next nodes" (bwd steps in fwd/bck analysis) */
202 
203  #define add_all_pos(it, target, source) \
204  for(std::set<nodet>::const_iterator \
205  it=(source).begin(); \
206  it!=(source).end(); ++it) \
207  (target).insert(*it);
208 
209  #ifdef CONTEXT_INSENSITIVE
210  /* to keep track of the functions (and their start/end nodes) */
211  std::stack<irep_idt> stack_fun;
212  irep_idt cur_fun;
213  std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
214  #endif
215 
216  /* current thread number */
217  unsigned thread;
218 
219  /* dependencies */
221 
222  /* writes and reads to unknown addresses -- conservative */
223  std::set<event_idt> unknown_read_nodes;
224  std::set<event_idt> unknown_write_nodes;
225 
226  /* set of functions visited so far -- we don't handle recursive functions */
227  std::set<irep_idt> functions_met;
228 
229  cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
230  :ns(_ns), instrumenter(_instrumenter), egraph(_instrumenter.egraph),
231  egraph_SCCs(_instrumenter.egraph_SCCs),
232  egraph_alt(_instrumenter.egraph_alt)
233  {
234  write_counter = 0;
235  read_counter = 0;
236  ws_counter = 0;
237  fr_rf_counter = 0;
238  thread = 0;
239  current_thread = 0;
240  max_thread = 0;
241  coming_from = 0;
242  }
243 
244  void inline enter_function(const irep_idt &function_id)
245  {
246  if(functions_met.find(function_id) != functions_met.end())
247  throw "sorry, doesn't handle recursive function for the moment";
248  functions_met.insert(function_id);
249  }
250 
251  void inline leave_function(const irep_idt &function_id)
252  {
253  functions_met.erase(function_id);
254  }
255 
256  void inline visit_cfg(
257  value_setst &value_sets,
258  memory_modelt model,
259  bool no_dependencies,
260  loop_strategyt duplicate_body,
261  const irep_idt &function_id)
262  {
263  /* ignore recursive calls -- underapproximation */
264  try
265  {
266  /* forbids recursive function */
267  enter_function(function_id);
268  std::set<nodet> end_out;
270  value_sets,
271  model,
272  no_dependencies,
273  duplicate_body,
274  function_id,
275  end_out);
276  leave_function(function_id);
277  }
278  catch(const std::string &s)
279  {
281  }
282  }
283 
292  virtual void visit_cfg_function(
293  value_setst &value_sets,
294  memory_modelt model,
295  bool no_dependencies,
296  loop_strategyt duplicate_body,
297  const irep_idt &function_id,
298  std::set<nodet> &ending_vertex);
299 
300  bool inline local(const irep_idt &i);
301  };
302 
303 public:
304  /* message */
306 
307  /* graph */
309 
310  /* graph split into strongly connected components */
311  std::vector<std::set<event_idt> > egraph_SCCs;
312 
313  /* critical cycles */
314  std::set<event_grapht::critical_cyclet> set_of_cycles;
315 
316  /* critical cycles per SCC */
317  std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
318  unsigned num_sccs;
319 
320  /* map from function to begin and end of the corresponding part of the
321  graph */
322  typedef std::map<irep_idt, std::pair<std::set<event_idt>,
323  std::set<event_idt> > > map_function_nodest;
325 
327  {
328  for(map_function_nodest::const_iterator it=map_function_graph.begin();
329  it!=map_function_graph.end();
330  ++it)
331  {
332  message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
333  message.debug() << "Start nodes: ";
334  for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
335  in_it!=it->second.first.end();
336  ++in_it)
337  message.debug() << *in_it << " ";
339  message.debug() << "End nodes: ";
340  for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
341  in_it!=it->second.second.end();
342  ++in_it)
343  message.debug() << *in_it << " ";
345  }
346  }
347 
348  /* variables to instrument, locations of variables to instrument on
349  the cycles, and locations of all the variables on the critical cycles */
350  /* TODO: those maps are here to interface easily with weak_mem.cpp,
351  but a rewriting of weak_mem can eliminate them */
352  std::set<irep_idt> var_to_instr;
353  std::multimap<irep_idt, source_locationt> id2loc;
354  std::multimap<irep_idt, source_locationt> id2cycloc;
355 
357  goto_modelt &_goto_model,
358  messaget &_message):
359  ns(_goto_model.symbol_table),
360  goto_functions(_goto_model.goto_functions),
361  render_po_aligned(true),
362  render_by_file(false),
363  render_by_function(false),
364  message(_message),
365  egraph(_message),
366  num_sccs(0)
367  {
368  }
369 
370  /* abstracts goto-programs in abstract event graph, and computes
371  the thread numbering and returns the max number */
372  unsigned goto2graph_cfg(
373  value_setst &value_sets,
374  memory_modelt model,
375  bool no_dependencies,
376  /* forces the duplication, with arrays or not; otherwise, arrays only */
377  loop_strategyt duplicate_body);
378 
379  /* collects directly all the cycles in the graph */
381  {
383  num_sccs = 0;
384  }
385 
386  /* collects the cycles in the graph by SCCs */
388 
389  /* filters cycles spurious by CFG */
390  void cfg_cycles_filter();
391 
392  /* sets parameters for collection, if required */
394  unsigned _max_var = 0,
395  unsigned _max_po_trans = 0,
396  bool _ignore_arrays = false)
397  {
398  egraph.set_parameters_collection(_max_var, _max_po_trans, _ignore_arrays);
399  }
400 
401  /* builds the relations between unsafe pairs in the critical cycles and
402  instructions to instrument in the code */
403 
404  /* strategies for instrumentation */
406  void instrument_my_events(const std::set<event_idt> &events);
407 
408  /* retrieves events to filter in the instrumentation choice
409  with option --my-events */
410  static std::set<event_idt> extract_my_events();
411 
412  /* sets rendering options */
413  void set_rendering_options(bool aligned, bool file, bool function)
414  {
415  render_po_aligned = aligned;
417  render_by_function = function;
418  assert(!render_by_file || !render_by_function);
419  }
420 
421  /* prints outputs:
422  - cycles.dot: graph of the instrumented cycles
423  - ref.txt: names of the instrumented cycles
424  - output.txt: names of the instructions in the code
425  - all.txt: all */
426  void print_outputs(memory_modelt model, bool hide_internals);
427 };
428 
429 #endif // CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
instrumentert::egraph_SCCs
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:311
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
instrumentert::cfg_visitort::visit_cfg_fence
void visit_cfg_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
Definition: goto2graph.cpp:1173
instrumentert::cfg_visitort::enter_function
void enter_function(const irep_idt &function_id)
Definition: goto2graph.h:244
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
instrumentert::print_map_function_graph
void print_map_function_graph() const
Definition: goto2graph.h:326
instrumentert::collect_cycles
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:380
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:317
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_id, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
Definition: goto2graph.cpp:148
instrumentert::cfg_visitort::thread
unsigned thread
Definition: goto2graph.h:217
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:582
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::fr_rf_counter
unsigned fr_rf_counter
Definition: goto2graph.h:190
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:1546
instrumentert::set_parameters_collection
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:393
dot
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
event_graph.h
graph of abstract events
grapht< abstract_eventt >
file
Definition: kdev_t.h:19
goto_model.h
Symbol Table + CFG.
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
goto_modelt
Definition: goto_model.h:26
instrumentert::cfg_visitort
Definition: goto2graph.h:90
instrumentert::map_function_nodest
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition: goto2graph.h:323
messaget::eom
static eomt eom
Definition: message.h:297
instrumentert::num_sccs
unsigned num_sccs
Definition: goto2graph.h:318
instrumentert::cfg_visitort::visit_cfg_body
void visit_cfg_body(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:464
instrumentert::cfg_visitort::visit_cfg_assign
void visit_cfg_assign(value_setst &value_sets, const irep_idt &function_id, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
Definition: goto2graph.cpp:840
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:316
instrumentert::cfg_visitort::incoming_post
std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
Definition: goto2graph.h:195
namespace.h
instrumentert::cfg_visitort::id2node_pairt
std::pair< irep_idt, event_idt > id2node_pairt
Definition: goto2graph.h:184
loop_strategyt
loop_strategyt
Definition: wmm.h:37
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:306
local_may_aliast
Definition: local_may_alias.h:26
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:88
instrumentert::id2loc
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:353
instrumentert::id2cycloc
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:354
instrumentert::ns
namespacet ns
Definition: goto2graph.h:36
instrumentert::cfg_visitort::updated
std::set< goto_programt::const_targett > updated
Definition: goto2graph.h:198
instrumentert::set_of_cyclest
std::set< event_grapht::critical_cyclet > set_of_cyclest
Definition: goto2graph.h:63
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:224
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:165
instrumentert::collect_cycles_by_SCCs
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
Definition: goto2graph.cpp:1601
instrumentert::cfg_visitort::contains_shared_array
bool contains_shared_array(const irep_idt &function_id, goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
Definition: goto2graph.cpp:408
instrumentert::set_rendering_options
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:413
instrumentert::cfg_visitort::leave_function
void leave_function(const irep_idt &function_id)
Definition: goto2graph.h:251
instrumentert::cfg_visitort::out_pos
incoming_post out_pos
Definition: goto2graph.h:201
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:185
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::~cfg_visitort
virtual ~cfg_visitort()
Definition: goto2graph.h:176
instrumentert::cost
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
Definition: instrumenter_strategies.cpp:178
instrumentert::cfg_visitort::coming_from
unsigned coming_from
Definition: goto2graph.h:102
instrumentert::cfg_visitort::max_thread
unsigned max_thread
Definition: goto2graph.h:180
instrumentert::local
bool local(const irep_idt &id)
is local variable?
Definition: goto2graph.cpp:33
instrumentert::cfg_visitort::in_pos
incoming_post in_pos
Definition: goto2graph.h:197
instrumentert::cfg_visitort::visit_cfg_asm_fence
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
Definition: goto2graph.cpp:787
instrumentert::map_function_graph
map_function_nodest map_function_graph
Definition: goto2graph.h:324
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:189
instrumentert::instrumentert
instrumentert(goto_modelt &_goto_model, messaget &_message)
Definition: goto2graph.h:356
instrumentert::cfg_visitort::egraph_alt
wmm_grapht & egraph_alt
Definition: goto2graph.h:98
instrumentert::cfg_visitort::visit_cfg_duplicate
void visit_cfg_duplicate(const goto_programt &goto_program, goto_programt::const_targett targ, goto_programt::const_targett i_it)
Definition: goto2graph.cpp:517
instrumentert::is_cfg_spurious
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
Definition: goto2graph.cpp:1251
memory_modelt
memory_modelt
Definition: wmm.h:18
instrumentert::cfg_visitort::map_writes
id2nodet map_writes
Definition: goto2graph.h:185
instrumentert
Definition: goto2graph.h:33
instrumentert::egraph
event_grapht egraph
Definition: goto2graph.h:308
instrumentert::add_instr_to_interleaving
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
Definition: goto2graph.cpp:1221
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
value_setst
Definition: value_sets.h:22
instrumentert::instrument_with_strategy
void instrument_with_strategy(instrumentation_strategyt strategy)
Definition: instrumenter_strategies.cpp:24
graph.h
A Template Class for Graphs.
instrumentert::map_vertex_gnode
std::map< event_idt, event_idt > map_vertex_gnode
Definition: goto2graph.h:42
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:305
event_grapht
Definition: event_graph.h:36
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_id)
Definition: goto2graph.h:256
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instrumentert::cfg_visitort::nodet
std::pair< event_idt, event_idt > nodet
Definition: goto2graph.h:193
instrumentert::cfg_visitort::data_dp
data_dpt data_dp
Definition: goto2graph.h:220
data_dpt
Definition: data_dp.h:52
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
instrumentation_strategyt
instrumentation_strategyt
Definition: wmm.h:27
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:429
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:227
wmm.h
memory models
event_grapht::critical_cyclet
Definition: event_graph.h:40
message.h
instrumentert::cfg_visitort::visit_cfg_propagate
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:294
all
@ all
Definition: wmm.h:28
instrumentert::cfg_visitort::egraph
event_grapht & egraph
Definition: goto2graph.h:96
messaget::warning
mstreamt & warning() const
Definition: message.h:404
instrumentert::cfg_cycles_filter
void cfg_cycles_filter()
Definition: goto2graph.cpp:1393
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:1440
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::cfg_visitort
cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
Definition: goto2graph.h:229
instrumentert::var_to_instr
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:352
instrumentert::cfg_visitort::write_counter
unsigned write_counter
Definition: goto2graph.h:187
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:314
instrumentert::cfg_visitort::visit_cfg_lwfence
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
Definition: goto2graph.cpp:748
instrumentert::cfg_visitort::visit_cfg_goto
void visit_cfg_goto(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
Definition: goto2graph.cpp:648
instrumentert::cfg_visitort::local
bool local(const irep_idt &i)
Definition: goto2graph.cpp:81
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:686
instrumentert::cfg_visitort::id2nodet
std::multimap< irep_idt, event_idt > id2nodet
Definition: goto2graph.h:183
instrumentert::cfg_visitort::unknown_read_nodes
std::set< event_idt > unknown_read_nodes
Definition: goto2graph.h:223
instrumentert::cfg_visitort::read_counter
unsigned read_counter
Definition: goto2graph.h:188
instrumentert::cfg_visitort::visit_cfg_skip
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:1215