cprover
fencer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fence inference: Main
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #include "fencer.h"
13 
14 #include <util/cprover_prefix.h>
15 #include <util/message.h>
16 
19 #include <goto-instrument/rw_set.h>
20 
21 #include "fence_inserter.h"
22 #include "fence_user_def.h"
23 #include "fence_assert.h"
24 
26  memory_modelt model,
27  value_setst &value_sets,
28  symbol_tablet &symbol_table,
29  goto_functionst &goto_functions,
30  bool SCC,
31  instrumentation_strategyt event_strategy,
32  unsigned unwinding_bound,
33  bool no_cfg_kill,
34  bool no_dependencies,
35  loop_strategyt duplicate_body,
36  unsigned input_max_var,
37  unsigned input_max_po_trans,
38  bool render_po,
39  bool render_file,
40  bool render_function,
41  bool cav11_option,
42  bool hide_internals,
43  bool print_graph,
44  infer_modet mode,
45  message_handlert &message_handler,
46  bool ignore_arrays)
47 {
48  messaget message(message_handler);
49 
50  message.status() << "--------" << messaget::eom;
51 
52  // all access to shared variables is pushed into assignments
53  Forall_goto_functions(f_it, goto_functions)
54  if(f_it->first!=CPROVER_PREFIX "initialize" &&
55  f_it->first!=goto_functionst::entry_point())
56  introduce_temporaries(value_sets, symbol_table, f_it->first,
57  f_it->second.body,
58 #ifdef LOCAL_MAY
59  f_it->second,
60 #endif
61  message);
62  message.status() << "Temporary variables added" << messaget::eom;
63 
64  unsigned max_thds = 0;
65  instrumentert instrumenter(symbol_table, goto_functions, message);
66  max_thds=instrumenter.goto2graph_cfg(value_sets, model,
67  no_dependencies, duplicate_body);
68  ++max_thds;
69  message.status() << "Abstract event graph computed" << messaget::eom;
70 
71  // collects cycles, directly or by SCCs
72  if(input_max_var!=0 || input_max_po_trans!=0)
73  instrumenter.set_parameters_collection(input_max_var, input_max_po_trans,
74  ignore_arrays);
75  else
76  instrumenter.set_parameters_collection(max_thds, 0, ignore_arrays);
77 
78  if(SCC)
79  {
80  instrumenter.collect_cycles_by_SCCs(model);
81  message.statistics() << "cycles collected: " << messaget::eom;
82  std::size_t interesting_scc = 0;
83  std::size_t total_cycles = 0;
84  for(std::size_t i=0; i<instrumenter.num_sccs; i++)
85  if(instrumenter.egraph_SCCs[i].size()>=4)
86  {
87  message.statistics() << "SCC #" << i << ": "
88  <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
89  <<" cycles found" << messaget::eom;
90  total_cycles += instrumenter
91  .set_of_cycles_per_SCC[interesting_scc++].size();
92  }
93 
94  /* if no cycle, no need to instrument */
95  if(total_cycles == 0)
96  {
97  message.result() << "program safe -- no need to place additional fences"
98  <<messaget::eom;
99 
100  // prints the whole abstract graph
101  if(print_graph)
102  instrumenter.egraph.print_graph();
103 
104  return;
105  }
106  }
107  else
108  {
109  instrumenter.collect_cycles(model);
110  message.statistics() << "cycles collected: "
111  << instrumenter.set_of_cycles.size()
112  << " cycles found" << messaget::eom;
113 
114  /* if no cycle, no need to instrument */
115  if(instrumenter.set_of_cycles.empty())
116  {
117  message.result()
118  << "program safe -- no need to place additional fences"
119  << messaget::eom;
120  instrumenter.print_map_function_graph();
121 
122  // prints the whole abstract graph
123  if(print_graph)
124  instrumenter.egraph.print_graph();
125 
126  return;
127  }
128  }
129 
130  /* selection of the cycles */
131  if(!no_cfg_kill)
132  instrumenter.cfg_cycles_filter();
133 
134  /* selects method, infers fences then outputs them */
135  switch(mode)
136  {
137  case INFER:
138  {
139  fence_insertert fence_inserter(instrumenter, model);
140  fence_inserter.compute();
141  fence_inserter.print_to_file_3();
142  break;
143  }
144  case USER_DEF:
145  {
146  fence_user_def_insertert fence_inserter(instrumenter, model);
147  fence_inserter.compute();
148  fence_inserter.print_to_file_3();
149  break;
150  }
151  case USER_ASSERT:
152  {
153  fence_assert_insertert fence_inserter(instrumenter, model);
154  fence_inserter.compute();
155  fence_inserter.print_to_file_3();
156  break;
157  }
158  }
159 
160  // additional outputs
161 #if 0
162  instrumenter.set_rendering_options(render_po, render_file, render_function);
163  instrumenter.print_outputs(model, hide_internals);
164 #endif
165 
166  /* TODO: insert the fences into the actual code or call script directly
167  from here*/
168 
169  /* removes potential skips */
170  Forall_goto_functions(f_it, goto_functions)
171  remove_skip(f_it->second.body);
172 
173  // update counters etc.
174  goto_functions.update();
175 
176  // prints the whole abstract graph
177  if(print_graph)
178  instrumenter.egraph.print_graph();
179 
180  // for debug only
181 #if 0
182  instrumenter.print_map_function_graph();
183 #endif
184 }
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
Fence inference.
instrumentation_strategyt
Definition: wmm.h:26
#define CPROVER_PREFIX
void introduce_temporaries(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:38
mstreamt & status()
Definition: message.h:238
void print_map_function_graph() const
Definition: goto2graph.h:301
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 fence_weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays)
Definition: fencer.cpp:25
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:349
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:382
memory_modelt
Definition: wmm.h:17
void print_graph()
Definition: event_graph.cpp:56
unsigned num_sccs
Definition: goto2graph.h:293
ILP construction for cycles affecting user-assertions and resolution.
Instrumenter.
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
The symbol table.
Definition: symbol_table.h:52
void cfg_cycles_filter()
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
ILP construction for all cycles and resolution.
ILP construction for cycles containing user-placed fences and resolution.
#define Forall_goto_functions(it, functions)
event_grapht egraph
Definition: goto2graph.h:283
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
Program Transformation.
infer_modet
Definition: infer_mode.h:13
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:286
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:292
Race Detection for Threaded Goto Programs.