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