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 symbol_tablet;
29 class goto_functionst;
30 class value_setst;
31 class local_may_aliast;
32 
34 {
35 public:
36  /* reference to goto-functions and symbol_table */
38 
39 protected:
41 
42  /* alternative representation of graph (SCC) */
43  std::map<event_idt, event_idt> map_vertex_gnode;
45 
46  unsigned unique_id;
47 
48  /* rendering options */
52 
53  bool inline local(const irep_idt &id);
54 
55  void inline add_instr_to_interleaving(
56  goto_programt::instructionst::iterator it,
57  goto_programt &interleaving);
58 
59  /* deprecated */
61 
63 
64  typedef std::set<event_grapht::critical_cyclet> set_of_cyclest;
65  void inline instrument_all_inserter(
66  const set_of_cyclest &set);
68  const set_of_cyclest &set);
70  const set_of_cyclest &set);
72  const set_of_cyclest &set);
74  const set_of_cyclest &set);
76  const set_of_cyclest &set, const std::set<event_idt> &events);
77 
78  void inline print_outputs_local(
79  const std::set<event_grapht::critical_cyclet> &set,
80  std::ofstream &dot,
81  std::ofstream &ref,
82  std::ofstream &output,
83  std::ofstream &all,
84  std::ofstream &table,
85  memory_modelt model,
86  bool hide_internals);
87 
88  typedef std::set<goto_programt::instructiont::targett> target_sett;
89 
91  {
92  protected:
95 
96  /* pointer to the egraph(s) that we construct */
98  std::vector<std::set<event_idt>> &egraph_SCCs;
100 
101  /* for thread marking (dynamic) */
102  unsigned current_thread;
103  unsigned coming_from;
104 
108  value_setst &value_sets
109  #ifdef LOCAL_MAY
110  , local_may_aliast local_may
111  #endif
112  ) const; // NOLINT(whitespace/parens)
113 
114  /* transformers */
115  void visit_cfg_thread() const;
116  void visit_cfg_propagate(goto_programt::instructionst::iterator i_it);
117  void visit_cfg_body(
119  loop_strategyt replicate_body,
120  value_setst &value_sets
121  #ifdef LOCAL_MAY
122  , local_may_aliast &local_may
123  #endif
124  ); // deprecated NOLINT(whitespace/parens)
129  void visit_cfg_assign(value_setst &value_sets, namespacet &ns,
130  goto_programt::instructionst::iterator &i_it, bool no_dependencies
131  #ifdef LOCAL_MAY
132  , local_may_aliast &local_may
133  #endif
134  ); // NOLINT(whitespace/parens)
135  void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
136  void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
137  void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it);
138  void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it);
139  void visit_cfg_function_call(value_setst &value_sets,
140  goto_programt::instructionst::iterator i_it,
141  memory_modelt model,
142  bool no_dependenciess,
143  loop_strategyt duplicate_body);
144  void visit_cfg_goto(
145  goto_programt::instructionst::iterator i_it,
146  /* forces the duplication of all the loops, with array or not
147  otherwise, duplication of loops with array accesses only */
148  loop_strategyt replicate_body,
149  value_setst &value_sets
150  #ifdef LOCAL_MAY
151  , local_may_aliast &local_may
152  #endif
153  ); // NOLINT(whitespace/parens)
155 
156  public:
157  virtual ~cfg_visitort()
158  {
159  }
160 
161  unsigned max_thread;
162 
163  /* relations between irep and Reads/Writes */
164  typedef std::multimap<irep_idt, event_idt> id2nodet;
165  typedef std::pair<irep_idt, event_idt> id2node_pairt;
167 
168  unsigned write_counter;
169  unsigned read_counter;
170  unsigned ws_counter;
171  unsigned fr_rf_counter;
172 
173  /* previous nodes (fwd analysis) */
174  typedef std::pair<event_idt, event_idt> nodet;
175  typedef std::map<goto_programt::const_targett, std::set<nodet> >
177 
179  std::set<goto_programt::const_targett> updated;
180 
181  /* "next nodes" (bwd steps in fwd/bck analysis) */
183 
184  #define add_all_pos(it, target, source) \
185  for(std::set<nodet>::const_iterator \
186  it=(source).begin(); \
187  it!=(source).end(); ++it) \
188  (target).insert(*it);
189 
190  #ifdef CONTEXT_INSENSITIVE
191  /* to keep track of the functions (and their start/end nodes) */
192  std::stack<irep_idt> stack_fun;
193  irep_idt cur_fun;
194  std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
195  #endif
196 
197  /* current thread number */
198  unsigned thread;
199 
200  /* dependencies */
202 
203  /* writes and reads to unknown addresses -- conservative */
204  std::set<event_idt> unknown_read_nodes;
205  std::set<event_idt> unknown_write_nodes;
206 
207  /* set of functions visited so far -- we don't handle recursive functions */
208  std::set<irep_idt> functions_met;
209 
210  cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
211  :ns(_ns), instrumenter(_instrumenter), egraph(_instrumenter.egraph),
212  egraph_SCCs(_instrumenter.egraph_SCCs),
213  egraph_alt(_instrumenter.egraph_alt)
214  {
215  write_counter = 0;
216  read_counter = 0;
217  ws_counter = 0;
218  fr_rf_counter = 0;
219  thread = 0;
220  current_thread = 0;
221  max_thread = 0;
222  coming_from = 0;
223  }
224 
225  void inline enter_function(const irep_idt &function)
226  {
227  if(functions_met.find(function)!=functions_met.end())
228  throw "sorry, doesn't handle recursive function for the moment";
229  functions_met.insert(function);
230  }
231 
232  void inline leave_function(const irep_idt &function)
233  {
234  functions_met.erase(function);
235  }
236 
237  void inline visit_cfg(
238  value_setst &value_sets,
239  memory_modelt model,
240  bool no_dependencies,
241  loop_strategyt duplicate_body,
242  const irep_idt &function)
243  {
244  /* ignore recursive calls -- underapproximation */
245  try
246  {
247  /* forbids recursive function */
248  enter_function(function);
249  const std::set<nodet> empty_in;
250  std::set<nodet> end_out;
251  visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
252  function, empty_in, end_out);
253  leave_function(function);
254  }
255  catch(std::string s)
256  {
257  instrumenter.message.warning() << s << messaget::eom;
258  }
259  }
260 
262  virtual void visit_cfg_function(
264  value_setst &value_sets,
265  memory_modelt model,
266  bool no_dependencies,
267  loop_strategyt duplicate_body,
269  const irep_idt &function,
271  const std::set<nodet> &initial_vertex,
273  std::set<nodet> &ending_vertex);
274 
275  bool inline local(const irep_idt &i);
276  };
277 
278 public:
279  /* message */
281 
282  /* graph */
284 
285  /* graph split into strongly connected components */
286  std::vector<std::set<event_idt> > egraph_SCCs;
287 
288  /* critical cycles */
289  std::set<event_grapht::critical_cyclet> set_of_cycles;
290 
291  /* critical cycles per SCC */
292  std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
293  unsigned num_sccs;
294 
295  /* map from function to begin and end of the corresponding part of the
296  graph */
297  typedef std::map<irep_idt, std::pair<std::set<event_idt>,
298  std::set<event_idt> > > map_function_nodest;
299  map_function_nodest map_function_graph;
300 
302  {
303  for(map_function_nodest::const_iterator it=map_function_graph.begin();
304  it!=map_function_graph.end();
305  ++it)
306  {
307  message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
308  message.debug() << "Start nodes: ";
309  for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
310  in_it!=it->second.first.end();
311  ++in_it)
312  message.debug() << *in_it << " ";
313  message.debug() << messaget::eom;
314  message.debug() << "End nodes: ";
315  for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
316  in_it!=it->second.second.end();
317  ++in_it)
318  message.debug() << *in_it << " ";
319  message.debug() << messaget::eom;
320  }
321  }
322 
323  /* variables to instrument, locations of variables to instrument on
324  the cycles, and locations of all the variables on the critical cycles */
325  /* TODO: those maps are here to interface easily with weak_mem.cpp,
326  but a rewriting of weak_mem can eliminate them */
327  std::set<irep_idt> var_to_instr;
328  std::multimap<irep_idt, source_locationt> id2loc;
329  std::multimap<irep_idt, source_locationt> id2cycloc;
330 
331  instrumentert(symbol_tablet &_symbol_table, goto_functionst &_goto_f,
332  messaget &_message)
333  :ns(_symbol_table), goto_functions(_goto_f), render_po_aligned(true),
334  render_by_file(false), render_by_function(false), message(_message),
335  egraph(_message)
336  {
337  }
338 
339  /* abstracts goto-programs in abstract event graph, and computes
340  the thread numbering and returns the max number */
341  unsigned goto2graph_cfg(
342  value_setst &value_sets,
343  memory_modelt model,
344  bool no_dependencies,
345  /* forces the duplication, with arrays or not; otherwise, arrays only */
346  loop_strategyt duplicate_body);
347 
348  /* collects directly all the cycles in the graph */
350  {
351  egraph.collect_cycles(set_of_cycles, model);
352  num_sccs = 0;
353  }
354 
355  /* collects the cycles in the graph by SCCs */
357 
358  /* filters cycles spurious by CFG */
359  void cfg_cycles_filter();
360 
361  /* sets parameters for collection, if required */
363  unsigned _max_var = 0,
364  unsigned _max_po_trans = 0,
365  bool _ignore_arrays = false)
366  {
367  egraph.set_parameters_collection(_max_var, _max_po_trans, _ignore_arrays);
368  }
369 
370  /* builds the relations between unsafe pairs in the critical cycles and
371  instructions to instrument in the code */
372 
373  /* strategies for instrumentation */
375  void instrument_my_events(const std::set<event_idt> &events);
376 
377  /* retrieves events to filter in the instrumentation choice
378  with option --my-events */
379  static std::set<event_idt> extract_my_events();
380 
381  /* sets rendering options */
382  void set_rendering_options(bool aligned, bool file, bool function)
383  {
384  render_po_aligned = aligned;
385  render_by_file = file;
386  render_by_function = function;
387  assert(!render_by_file || !render_by_function);
388  }
389 
390  /* prints outputs:
391  - cycles.dot: graph of the instrumented cycles
392  - ref.txt: names of the instrumented cycles
393  - output.txt: names of the instructions in the code
394  - all.txt: all */
395  void print_outputs(memory_modelt model, bool hide_internals);
396 };
397 
398 #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:93
mstreamt & warning()
Definition: message.h:228
void visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it)
Definition: goto2graph.cpp:499
std::set< event_idt > unknown_read_nodes
Definition: goto2graph.h:204
std::map< event_idt, event_idt > map_vertex_gnode
Definition: goto2graph.h:43
std::multimap< irep_idt, event_idt > id2nodet
Definition: goto2graph.h:164
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:327
bool render_by_file
Definition: goto2graph.h:50
memory models
goto_functionst & goto_functions
Definition: goto2graph.h:40
instrumentation_strategyt
Definition: wmm.h:26
messaget & message
Definition: goto2graph.h:280
instrumentert(symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &_message)
Definition: goto2graph.h:331
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:725
void print_map_function_graph() const
Definition: goto2graph.h:301
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:528
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:64
std::set< irep_idt > functions_met
Definition: goto2graph.h:208
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
unsigned unique_id
Definition: goto2graph.h:46
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
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:313
namespacet ns
Definition: goto2graph.h:37
std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
Definition: goto2graph.h:176
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:349
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:658
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:382
bool render_by_function
Definition: goto2graph.h:51
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:454
instructionst::const_iterator const_targett
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:153
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition: goto2graph.h:298
std::pair< event_idt, event_idt > nodet
Definition: goto2graph.h:174
bool local(const irep_idt &id)
is local variable?
Definition: goto2graph.cpp:38
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:86
void enter_function(const irep_idt &function)
Definition: goto2graph.h:225
unsigned num_sccs
Definition: goto2graph.h:293
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:328
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:329
void leave_function(const irep_idt &function)
Definition: goto2graph.h:232
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:563
std::set< goto_programt::instructiont::targett > target_sett
Definition: goto2graph.h:88
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function)
Definition: goto2graph.h:237
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
instrumentert & instrumenter
Definition: goto2graph.h:94
A Template Class for Graphs.
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
mstreamt & debug()
Definition: message.h:253
map_function_nodest map_function_graph
Definition: goto2graph.h:299
bool contains_shared_array(goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
Definition: goto2graph.cpp:405
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:757
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:513
cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
Definition: goto2graph.h:210
std::vector< std::set< event_idt > > & egraph_SCCs
Definition: goto2graph.h:98
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
event_grapht egraph
Definition: goto2graph.h:283
std::set< event_idt > unknown_write_nodes
Definition: goto2graph.h:205
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
std::set< goto_programt::const_targett > updated
Definition: goto2graph.h:179
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
Definition: dot.cpp:353
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:289
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:362
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:291
wmm_grapht egraph_alt
Definition: goto2graph.h:44
std::pair< irep_idt, event_idt > id2node_pairt
Definition: goto2graph.h:165
void visit_cfg_fence(goto_programt::instructionst::iterator i_it)
Concrete Goto Program.
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:286
void visit_cfg_assign(value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
Definition: goto2graph.cpp:797
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:292
bool render_po_aligned
Definition: goto2graph.h:49
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:629