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/fresh_symbol.h>
27 
29 
31 
32 #include <goto-instrument/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_id,
42  goto_programt &goto_program,
43 #ifdef LOCAL_MAY
44  const goto_functionst::goto_functiont &goto_function,
45 #endif
47 {
48  namespacet ns(symbol_table);
49 
50 #ifdef LOCAL_MAY
51  local_may_aliast local_may(goto_function);
52 #endif
53 
54  Forall_goto_program_instructions(i_it, goto_program)
55  {
56  goto_programt::instructiont &instruction=*i_it;
57 
58  message.debug() <<instruction.source_location<< messaget::eom;
59 
60  if(instruction.is_goto() ||
61  instruction.is_assert() ||
62  instruction.is_assume())
63  {
64  rw_set_loct rw_set(
65  ns,
66  value_sets,
67  function_id,
68  i_it
69 #ifdef LOCAL_MAY
70  ,
71  local_may
72 #endif
73  ); // NOLINT(whitespace/parens)
74  if(rw_set.empty())
75  continue;
76 
77  symbolt &new_symbol = get_fresh_aux_symbol(
78  bool_typet(),
79  id2string(function_id),
80  "$tmp_guard",
81  instruction.source_location,
82  ns.lookup(function_id).mode,
83  symbol_table);
84  new_symbol.is_static_lifetime=true;
85  new_symbol.is_thread_local=true;
86  new_symbol.value.make_nil();
87 
88  symbol_exprt symbol_expr=new_symbol.symbol_expr();
89 
91  code_assignt(symbol_expr, instruction.get_condition()),
92  instruction.source_location);
93 
94  // replace guard
95  instruction.set_condition(symbol_expr);
96  goto_program.insert_before_swap(i_it, new_i);
97 
98  i_it++; // step forward
99  }
100  else if(instruction.is_function_call())
101  {
102  // nothing
103  }
104  }
105 }
106 
108  memory_modelt model,
109  value_setst &value_sets,
110  goto_modelt &goto_model,
111  bool SCC,
112  instrumentation_strategyt event_strategy,
113  bool no_cfg_kill,
114  bool no_dependencies,
115  loop_strategyt duplicate_body,
116  unsigned input_max_var,
117  unsigned input_max_po_trans,
118  bool render_po,
119  bool render_file,
120  bool render_function,
121  bool cav11_option,
122  bool hide_internals,
123  message_handlert &message_handler,
124  bool ignore_arrays)
125 {
126  messaget message(message_handler);
127 
128  // no more used -- dereferences performed in rw_set
129  // get rid of pointers
130  // remove_pointers(goto_functions, symbol_table, value_sets);
131  // add_failed_symbols(symbol_table);
132  // message.status() <<"pointers removed"<< messaget::eom;
133 
134  message.status() << "--------" << messaget::eom;
135 
136  // all access to shared variables is pushed into assignments
137  Forall_goto_functions(f_it, goto_model.goto_functions)
138  if(f_it->first != INITIALIZE_FUNCTION &&
139  f_it->first!=goto_functionst::entry_point())
140  introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first,
141  f_it->second.body,
142 #ifdef LOCAL_MAY
143  f_it->second,
144 #endif
145  message);
146 
147  message.status() << "Temp added" << messaget::eom;
148 
149  unsigned max_thds = 0;
150  instrumentert instrumenter(goto_model, message);
151  max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies,
152  duplicate_body);
153  message.status()<<"abstraction completed"<<messaget::eom;
154 
155  // collects cycles, directly or by SCCs
156  if(input_max_var!=0 || input_max_po_trans!=0)
157  instrumenter.set_parameters_collection(input_max_var,
158  input_max_po_trans, ignore_arrays);
159  else
160  instrumenter.set_parameters_collection(max_thds, 0, ignore_arrays);
161 
162  if(SCC)
163  {
164  instrumenter.collect_cycles_by_SCCs(model);
165  message.status()<<"cycles collected: "<<messaget::eom;
166  unsigned interesting_scc = 0;
167  unsigned total_cycles = 0;
168  for(unsigned i=0; i<instrumenter.num_sccs; i++)
169  if(instrumenter.egraph_SCCs[i].size()>=4)
170  {
171  message.status()<<"SCC #"<<i<<": "
172  <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
173  <<" cycles found"<<messaget::eom;
174  total_cycles += instrumenter
175  .set_of_cycles_per_SCC[interesting_scc++].size();
176  }
177 
178  /* if no cycle, no need to instrument */
179  if(total_cycles == 0)
180  {
181  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
182  return;
183  }
184  }
185  else
186  {
187  instrumenter.collect_cycles(model);
188  message.status()<<"cycles collected: "<<instrumenter.set_of_cycles.size()
189  <<" cycles found"<<messaget::eom;
190 
191  /* if no cycle, no need to instrument */
192  if(instrumenter.set_of_cycles.empty())
193  {
194  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
195  return;
196  }
197  }
198 
199  if(!no_cfg_kill)
200  instrumenter.cfg_cycles_filter();
201 
202  // collects instructions to instrument, depending on the strategy selected
203  if(event_strategy == my_events)
204  {
205  const std::set<event_idt> events_set = instrumentert::extract_my_events();
206  instrumenter.instrument_my_events(events_set);
207  }
208  else
209  instrumenter.instrument_with_strategy(event_strategy);
210 
211  // prints outputs
212  instrumenter.set_rendering_options(render_po, render_file, render_function);
213  instrumenter.print_outputs(model, hide_internals);
214 
215  // now adds buffers
216  shared_bufferst shared_buffers(
217  goto_model.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(value_sets, goto_model.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 
249  shared_buffers, goto_model.symbol_table, goto_model.goto_functions);
250  visitor.weak_memory(
251  value_sets, goto_model.goto_functions.entry_point(), model);
252 
253  /* removes potential skips */
254  remove_skip(goto_model);
255 
256  // initialization code for buffers
257  shared_buffers.add_initialization_code(goto_model.goto_functions);
258 
259  // update counters etc.
260  goto_model.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:88
void add_initialization_code(goto_functionst &goto_functions)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:42
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:628
bool is_thread_local
Definition: symbol.h:65
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:352
instrumentation_strategyt
Definition: wmm.h:26
bool empty() const
Definition: rw_set.h:75
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Fresh auxiliary symbol creation.
void introduce_temporaries(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:38
exprt value
Initial value of symbol.
Definition: symbol.h:34
The Boolean type.
Definition: std_types.h:29
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
Symbol table entry.
Definition: symbol.h:27
void print_outputs(memory_modelt model, bool hide_internals)
Weak Memory Instrumentation for Threaded Goto Programs.
loop_strategyt
Definition: wmm.h:36
void affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
bool is_static_lifetime
Definition: symbol.h:65
void set_cav11(memory_modelt model)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:380
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:413
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
memory_modelt
Definition: wmm.h:17
void instrument_my_events(const std::set< event_idt > &events)
std::multimap< irep_idt, source_locationt > cycles_r_loc
unsigned num_sccs
Definition: goto2graph.h:318
Instrumenter.
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
#define INITIALIZE_FUNCTION
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:353
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
::goto_functiont goto_functiont
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:354
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:146
void instrument_with_strategy(instrumentation_strategyt strategy)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
void cfg_cycles_filter()
std::multimap< irep_idt, source_locationt > cycles_loc
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static eomt eom
Definition: message.h:278
Definition: wmm.h:32
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
static std::set< event_idt > extract_my_events()
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
#define Forall_goto_functions(it, functions)
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, 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::set< irep_idt > cycles
void make_nil()
Definition: irep.h:470
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:314
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:393
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Definition: std_expr.h:102
std::set< irep_idt > affected_by_delay_set
Program Transformation.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:311
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
A codet representing an assignment in the program.
Definition: std_code.h:297
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:317
Race Detection for Threaded Goto Programs.
void weak_memory(value_setst &value_sets, const irep_idt &function_id, memory_modelt model)
instruments the program for the pairs detected through the CFG