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(value_setst &value_sets, namespacet &ns,
129  goto_programt::instructionst::iterator &i_it, bool no_dependencies
130  #ifdef LOCAL_MAY
131  , local_may_aliast &local_may
132  #endif
133  ); // NOLINT(whitespace/parens)
134  void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
135  void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
136  void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it);
137  void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it);
138  void visit_cfg_function_call(value_setst &value_sets,
139  goto_programt::instructionst::iterator i_it,
140  memory_modelt model,
141  bool no_dependenciess,
142  loop_strategyt duplicate_body);
143  void visit_cfg_goto(
144  goto_programt::instructionst::iterator i_it,
145  /* forces the duplication of all the loops, with array or not
146  otherwise, duplication of loops with array accesses only */
147  loop_strategyt replicate_body,
148  value_setst &value_sets
149  #ifdef LOCAL_MAY
150  , local_may_aliast &local_may
151  #endif
152  ); // NOLINT(whitespace/parens)
154 
155  public:
156  virtual ~cfg_visitort()
157  {
158  }
159 
160  unsigned max_thread;
161 
162  /* relations between irep and Reads/Writes */
163  typedef std::multimap<irep_idt, event_idt> id2nodet;
164  typedef std::pair<irep_idt, event_idt> id2node_pairt;
166 
167  unsigned write_counter;
168  unsigned read_counter;
169  unsigned ws_counter;
170  unsigned fr_rf_counter;
171 
172  /* previous nodes (fwd analysis) */
173  typedef std::pair<event_idt, event_idt> nodet;
174  typedef std::map<goto_programt::const_targett, std::set<nodet> >
176 
178  std::set<goto_programt::const_targett> updated;
179 
180  /* "next nodes" (bwd steps in fwd/bck analysis) */
182 
183  #define add_all_pos(it, target, source) \
184  for(std::set<nodet>::const_iterator \
185  it=(source).begin(); \
186  it!=(source).end(); ++it) \
187  (target).insert(*it);
188 
189  #ifdef CONTEXT_INSENSITIVE
190  /* to keep track of the functions (and their start/end nodes) */
191  std::stack<irep_idt> stack_fun;
192  irep_idt cur_fun;
193  std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
194  #endif
195 
196  /* current thread number */
197  unsigned thread;
198 
199  /* dependencies */
201 
202  /* writes and reads to unknown addresses -- conservative */
203  std::set<event_idt> unknown_read_nodes;
204  std::set<event_idt> unknown_write_nodes;
205 
206  /* set of functions visited so far -- we don't handle recursive functions */
207  std::set<irep_idt> functions_met;
208 
209  cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
210  :ns(_ns), instrumenter(_instrumenter), egraph(_instrumenter.egraph),
211  egraph_SCCs(_instrumenter.egraph_SCCs),
212  egraph_alt(_instrumenter.egraph_alt)
213  {
214  write_counter = 0;
215  read_counter = 0;
216  ws_counter = 0;
217  fr_rf_counter = 0;
218  thread = 0;
219  current_thread = 0;
220  max_thread = 0;
221  coming_from = 0;
222  }
223 
224  void inline enter_function(const irep_idt &function)
225  {
226  if(functions_met.find(function)!=functions_met.end())
227  throw "sorry, doesn't handle recursive function for the moment";
228  functions_met.insert(function);
229  }
230 
231  void inline leave_function(const irep_idt &function)
232  {
233  functions_met.erase(function);
234  }
235 
236  void inline visit_cfg(
237  value_setst &value_sets,
238  memory_modelt model,
239  bool no_dependencies,
240  loop_strategyt duplicate_body,
241  const irep_idt &function)
242  {
243  /* ignore recursive calls -- underapproximation */
244  try
245  {
246  /* forbids recursive function */
247  enter_function(function);
248  const std::set<nodet> empty_in;
249  std::set<nodet> end_out;
250  visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
251  function, empty_in, end_out);
252  leave_function(function);
253  }
254  catch(const std::string &s)
255  {
257  }
258  }
259 
261  virtual void visit_cfg_function(
263  value_setst &value_sets,
264  memory_modelt model,
265  bool no_dependencies,
266  loop_strategyt duplicate_body,
268  const irep_idt &function,
270  const std::set<nodet> &initial_vertex,
272  std::set<nodet> &ending_vertex);
273 
274  bool inline local(const irep_idt &i);
275  };
276 
277 public:
278  /* message */
280 
281  /* graph */
283 
284  /* graph split into strongly connected components */
285  std::vector<std::set<event_idt> > egraph_SCCs;
286 
287  /* critical cycles */
288  std::set<event_grapht::critical_cyclet> set_of_cycles;
289 
290  /* critical cycles per SCC */
291  std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
292  unsigned num_sccs;
293 
294  /* map from function to begin and end of the corresponding part of the
295  graph */
296  typedef std::map<irep_idt, std::pair<std::set<event_idt>,
297  std::set<event_idt> > > map_function_nodest;
299 
301  {
302  for(map_function_nodest::const_iterator it=map_function_graph.begin();
303  it!=map_function_graph.end();
304  ++it)
305  {
306  message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
307  message.debug() << "Start nodes: ";
308  for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
309  in_it!=it->second.first.end();
310  ++in_it)
311  message.debug() << *in_it << " ";
313  message.debug() << "End nodes: ";
314  for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
315  in_it!=it->second.second.end();
316  ++in_it)
317  message.debug() << *in_it << " ";
319  }
320  }
321 
322  /* variables to instrument, locations of variables to instrument on
323  the cycles, and locations of all the variables on the critical cycles */
324  /* TODO: those maps are here to interface easily with weak_mem.cpp,
325  but a rewriting of weak_mem can eliminate them */
326  std::set<irep_idt> var_to_instr;
327  std::multimap<irep_idt, source_locationt> id2loc;
328  std::multimap<irep_idt, source_locationt> id2cycloc;
329 
331  goto_modelt &_goto_model,
332  messaget &_message):
333  ns(_goto_model.symbol_table),
334  goto_functions(_goto_model.goto_functions),
335  render_po_aligned(true),
336  render_by_file(false),
337  render_by_function(false),
338  message(_message),
339  egraph(_message),
340  num_sccs(0)
341  {
342  }
343 
344  /* abstracts goto-programs in abstract event graph, and computes
345  the thread numbering and returns the max number */
346  unsigned goto2graph_cfg(
347  value_setst &value_sets,
348  memory_modelt model,
349  bool no_dependencies,
350  /* forces the duplication, with arrays or not; otherwise, arrays only */
351  loop_strategyt duplicate_body);
352 
353  /* collects directly all the cycles in the graph */
355  {
357  num_sccs = 0;
358  }
359 
360  /* collects the cycles in the graph by SCCs */
362 
363  /* filters cycles spurious by CFG */
364  void cfg_cycles_filter();
365 
366  /* sets parameters for collection, if required */
368  unsigned _max_var = 0,
369  unsigned _max_po_trans = 0,
370  bool _ignore_arrays = false)
371  {
372  egraph.set_parameters_collection(_max_var, _max_po_trans, _ignore_arrays);
373  }
374 
375  /* builds the relations between unsafe pairs in the critical cycles and
376  instructions to instrument in the code */
377 
378  /* strategies for instrumentation */
380  void instrument_my_events(const std::set<event_idt> &events);
381 
382  /* retrieves events to filter in the instrumentation choice
383  with option --my-events */
384  static std::set<event_idt> extract_my_events();
385 
386  /* sets rendering options */
387  void set_rendering_options(bool aligned, bool file, bool function)
388  {
389  render_po_aligned = aligned;
391  render_by_function = function;
392  assert(!render_by_file || !render_by_function);
393  }
394 
395  /* prints outputs:
396  - cycles.dot: graph of the instrumented cycles
397  - ref.txt: names of the instrumented cycles
398  - output.txt: names of the instructions in the code
399  - all.txt: all */
400  void print_outputs(memory_modelt model, bool hide_internals);
401 };
402 
403 #endif // CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
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
void visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it)
Definition: goto2graph.cpp:493
std::set< event_idt > unknown_read_nodes
Definition: goto2graph.h:203
std::map< event_idt, event_idt > map_vertex_gnode
Definition: goto2graph.h:42
std::multimap< irep_idt, event_idt > id2nodet
Definition: goto2graph.h:163
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:326
bool render_by_file
Definition: goto2graph.h:49
memory models
goto_functionst & goto_functions
Definition: goto2graph.h:39
instrumentation_strategyt
Definition: wmm.h:26
messaget & message
Definition: goto2graph.h:279
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:719
void print_map_function_graph() const
Definition: goto2graph.h:300
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: event_graph.h:568
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
graph of abstract events
void instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)
std::set< event_grapht::critical_cyclet > set_of_cyclest
Definition: goto2graph.h:63
std::set< irep_idt > functions_met
Definition: goto2graph.h:207
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
unsigned unique_id
Definition: goto2graph.h:45
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void print_outputs(memory_modelt model, bool hide_internals)
loop_strategyt
Definition: wmm.h:36
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
Definition: goto2graph.cpp:307
namespacet ns
Definition: goto2graph.h:36
std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
Definition: goto2graph.h:175
mstreamt & warning() const
Definition: message.h:307
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:354
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:652
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:387
bool render_by_function
Definition: goto2graph.h:50
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:448
Symbol Table + CFG.
virtual void visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, const std::set< nodet > &initial_vertex, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
Definition: goto2graph.cpp:147
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition: goto2graph.h:297
std::pair< event_idt, event_idt > nodet
Definition: goto2graph.h:173
bool local(const irep_idt &id)
is local variable?
Definition: goto2graph.cpp:32
memory_modelt
Definition: wmm.h:17
void instrument_my_events(const std::set< event_idt > &events)
bool local(const irep_idt &i)
Definition: goto2graph.cpp:80
void enter_function(const irep_idt &function)
Definition: goto2graph.h:224
unsigned num_sccs
Definition: goto2graph.h:292
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
instrumentert(goto_modelt &_goto_model, messaget &_message)
Definition: goto2graph.h:330
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:327
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:328
void leave_function(const irep_idt &function)
Definition: goto2graph.h:231
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:557
std::set< goto_programt::instructiont::targett > target_sett
Definition: goto2graph.h:87
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function)
Definition: goto2graph.h:236
void instrument_with_strategy(instrumentation_strategyt strategy)
void cfg_cycles_filter()
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)
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
instrumentert & instrumenter
Definition: goto2graph.h:93
A Template Class for Graphs.
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
map_function_nodest map_function_graph
Definition: goto2graph.h:298
bool contains_shared_array(goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
Definition: goto2graph.cpp:399
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:751
void instrument_all_inserter(const set_of_cyclest &set)
static std::set< event_idt > extract_my_events()
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Definition: event_graph.h:553
cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
Definition: goto2graph.h:209
std::vector< std::set< event_idt > > & egraph_SCCs
Definition: goto2graph.h:97
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
event_grapht egraph
Definition: goto2graph.h:282
std::set< event_idt > unknown_write_nodes
Definition: goto2graph.h:204
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
std::set< goto_programt::const_targett > updated
Definition: goto2graph.h:178
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:288
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:367
mstreamt & debug() const
Definition: message.h:332
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:285
wmm_grapht egraph_alt
Definition: goto2graph.h:43
std::pair< irep_idt, event_idt > id2node_pairt
Definition: goto2graph.h:164
void visit_cfg_fence(goto_programt::instructionst::iterator i_it)
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:285
void visit_cfg_assign(value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
Definition: goto2graph.cpp:791
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:291
bool render_po_aligned
Definition: goto2graph.h:48
Definition: wmm.h:28
Definition: kdev_t.h:19
void visit_cfg_goto(goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
Definition: goto2graph.cpp:623