cprover
weak_memory.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Weak Memory Instrumentation for Threaded Goto Programs
4 
5 Author: Daniel Kroening, Vincent Nimal
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 /*
15  * Strategy: we first overapproximate all the read/write sequences of
16  * the program executions with a read/write graph. We then detect the
17  * pairs potentially dangerous, and to be delayed in some executions
18  * of the program. We finally insert the corresponding instrumentations
19  * in the program.
20  */
21 
22 #include "weak_memory.h"
23 
24 #include <set>
25 
26 #include <util/cprover_prefix.h>
27 #include <util/prefix.h>
28 #include <util/message.h>
29 
31 
32 #include "../rw_set.h"
33 
34 #include "shared_buffers.h"
35 #include "goto2graph.h"
36 
39  value_setst &value_sets,
40  symbol_tablet &symbol_table,
41  const irep_idt &function,
42  goto_programt &goto_program,
43 #ifdef LOCAL_MAY
44  const goto_functionst::goto_functiont &goto_function,
45 #endif
46  messaget &message)
47 {
48  namespacet ns(symbol_table);
49  unsigned tmp_counter=0;
50 
51 #ifdef LOCAL_MAY
52  local_may_aliast local_may(goto_function);
53 #endif
54 
55  Forall_goto_program_instructions(i_it, goto_program)
56  {
57  goto_programt::instructiont &instruction=*i_it;
58 
59  message.debug() <<instruction.source_location<< messaget::eom;
60 
61  if(instruction.is_goto() ||
62  instruction.is_assert() ||
63  instruction.is_assume())
64  {
65  rw_set_loct rw_set(ns, value_sets, i_it
66 #ifdef LOCAL_MAY
67  , local_may
68 #endif
69  ); // NOLINT(whitespace/parens)
70  if(rw_set.empty())
71  continue;
72 
73  symbolt new_symbol;
74  new_symbol.base_name="$tmp_guard";
75  new_symbol.name=
76  id2string(function)+"$tmp_guard"+std::to_string(tmp_counter++);
77  new_symbol.type=bool_typet();
78  new_symbol.is_static_lifetime=true;
79  new_symbol.is_thread_local=true;
80  new_symbol.value.make_nil();
81 
82  symbol_exprt symbol_expr=new_symbol.symbol_expr();
83 
84  symbolt *symbol_ptr;
85  symbol_table.move(new_symbol, symbol_ptr);
86 
87  goto_programt::instructiont new_i;
88  new_i.make_assignment();
89  new_i.code=code_assignt(symbol_expr, instruction.guard);
90  new_i.source_location=instruction.source_location;
91  new_i.function=instruction.function;
92 
93  // replace guard
94  instruction.guard=symbol_expr;
95  goto_program.insert_before_swap(i_it, new_i);
96 
97  i_it++; // step forward
98  }
99  else if(instruction.is_function_call())
100  {
101  // nothing
102  }
103  }
104 }
105 
107  memory_modelt model,
108  value_setst &value_sets,
109  symbol_tablet &symbol_table,
110  goto_functionst &goto_functions,
111  bool SCC,
112  instrumentation_strategyt event_strategy,
113  unsigned unwinding_bound,
114  bool no_cfg_kill,
115  bool no_dependencies,
116  loop_strategyt duplicate_body,
117  unsigned input_max_var,
118  unsigned input_max_po_trans,
119  bool render_po,
120  bool render_file,
121  bool render_function,
122  bool cav11_option,
123  bool hide_internals,
124  message_handlert &message_handler,
125  bool ignore_arrays)
126 {
127  messaget message(message_handler);
128 
129  // no more used -- dereferences performed in rw_set
130  // get rid of pointers
131  // remove_pointers(goto_functions, symbol_table, value_sets);
132  // add_failed_symbols(symbol_table);
133  // message.status() <<"pointers removed"<< messaget::eom;
134 
135  message.status() << "--------" << messaget::eom;
136 
137  // all access to shared variables is pushed into assignments
138  Forall_goto_functions(f_it, goto_functions)
139  if(f_it->first!=CPROVER_PREFIX "initialize" &&
140  f_it->first!=goto_functionst::entry_point())
141  introduce_temporaries(value_sets, symbol_table, f_it->first,
142  f_it->second.body,
143 #ifdef LOCAL_MAY
144  f_it->second,
145 #endif
146  message);
147 
148  message.status() << "Temp added" << messaget::eom;
149 
150  unsigned max_thds = 0;
151  instrumentert instrumenter(symbol_table, goto_functions, message);
152  max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies,
153  duplicate_body);
154  message.status()<<"abstraction completed"<<messaget::eom;
155 
156  // collects cycles, directly or by SCCs
157  if(input_max_var!=0 || input_max_po_trans!=0)
158  instrumenter.set_parameters_collection(input_max_var,
159  input_max_po_trans, ignore_arrays);
160  else
161  instrumenter.set_parameters_collection(max_thds, ignore_arrays);
162 
163  if(SCC)
164  {
165  instrumenter.collect_cycles_by_SCCs(model);
166  message.status()<<"cycles collected: "<<messaget::eom;
167  unsigned interesting_scc = 0;
168  unsigned total_cycles = 0;
169  for(unsigned i=0; i<instrumenter.num_sccs; i++)
170  if(instrumenter.egraph_SCCs[i].size()>=4)
171  {
172  message.status()<<"SCC #"<<i<<": "
173  <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
174  <<" cycles found"<<messaget::eom;
175  total_cycles += instrumenter
176  .set_of_cycles_per_SCC[interesting_scc++].size();
177  }
178 
179  /* if no cycle, no need to instrument */
180  if(total_cycles == 0)
181  {
182  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
183  return;
184  }
185  }
186  else
187  {
188  instrumenter.collect_cycles(model);
189  message.status()<<"cycles collected: "<<instrumenter.set_of_cycles.size()
190  <<" cycles found"<<messaget::eom;
191 
192  /* if no cycle, no need to instrument */
193  if(instrumenter.set_of_cycles.empty())
194  {
195  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
196  return;
197  }
198  }
199 
200  if(!no_cfg_kill)
201  instrumenter.cfg_cycles_filter();
202 
203  // collects instructions to instrument, depending on the strategy selected
204  if(event_strategy == my_events)
205  {
206  const std::set<event_idt> events_set = instrumentert::extract_my_events();
207  instrumenter.instrument_my_events(events_set);
208  }
209  else
210  instrumenter.instrument_with_strategy(event_strategy);
211 
212  // prints outputs
213  instrumenter.set_rendering_options(render_po, render_file, render_function);
214  instrumenter.print_outputs(model, hide_internals);
215 
216  // now adds buffers
217  shared_bufferst shared_buffers(symbol_table, max_thds, message);
218 
219  if(cav11_option)
220  shared_buffers.set_cav11(model);
221 
222  // stores the events to instrument
223  shared_buffers.cycles = instrumenter.var_to_instr; // var in the cycles
224  shared_buffers.cycles_loc = instrumenter.id2loc; // instrumented places
225  shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles
226 
227  // for reads delays
228  shared_buffers.affected_by_delay(symbol_table, value_sets, goto_functions);
229 
230  for(std::set<irep_idt>::iterator it=
231  shared_buffers.affected_by_delay_set.begin();
232  it!=shared_buffers.affected_by_delay_set.end();
233  it++)
234  message.debug()<<id2string(*it)<<messaget::eom;
235 
236  message.status()<<"I instrument:"<<messaget::eom;
237  for(std::set<irep_idt>::iterator it=shared_buffers.cycles.begin();
238  it!=shared_buffers.cycles.end(); it++)
239  {
240  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
241  const std::pair<m_itt, m_itt> ran=
242  shared_buffers.cycles_loc.equal_range(*it);
243  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
244  message.result() << ((*it)==""?"fence":*it) << ", "
245  << ran_it->second << messaget::eom;
246  }
247 
248  shared_bufferst::cfg_visitort visitor(shared_buffers, symbol_table,
249  goto_functions);
250  visitor.weak_memory(value_sets, goto_functions.entry_point(), model);
251 
252  /* removes potential skips */
253  Forall_goto_functions(f_it, goto_functions)
254  remove_skip(f_it->second.body);
255 
256  // initialization code for buffers
257  shared_buffers.add_initialization_code(goto_functions);
258 
259  // update counters etc.
260  goto_functions.update();
261 
262  message.status()<< "Goto-program instrumented" << messaget::eom;
263 }
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
void add_initialization_code(goto_functionst &goto_functions)
irep_idt name
The unique identifier.
Definition: symbol.h:46
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:70
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:327
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
bool empty() const
Definition: rw_set.h:72
mstreamt & status()
Definition: message.h:238
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
exprt value
Initial value of symbol.
Definition: symbol.h:40
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void print_outputs(memory_modelt model, bool hide_internals)
Weak Memory Instrumentation for Threaded Goto Programs.
loop_strategyt
Definition: wmm.h:36
bool is_static_lifetime
Definition: symbol.h:70
void set_cav11(memory_modelt model)
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:349
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:382
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
memory_modelt
Definition: wmm.h:17
void instrument_my_events(const std::set< event_idt > &events)
void affected_by_delay(symbol_tablet &symbol_table, value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
std::multimap< irep_idt, source_locationt > cycles_r_loc
unsigned num_sccs
Definition: goto2graph.h:293
Instrumenter.
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
goto_function_templatet< goto_programt > goto_functiont
void instrument_with_strategy(instrumentation_strategyt strategy)
void cfg_cycles_filter()
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void 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, message_handlert &message_handler, bool ignore_arrays)
std::multimap< irep_idt, source_locationt > cycles_loc
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Definition: wmm.h:32
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
static std::set< event_idt > extract_my_events()
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
#define Forall_goto_functions(it, functions)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::set< irep_idt > cycles
void make_nil()
Definition: irep.h:243
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
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::set< irep_idt > affected_by_delay_set
Program Transformation.
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:286
Assignment.
Definition: std_code.h:144
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:292