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 
27 
29 
30 #include <goto-instrument/rw_set.h>
31 
32 #include "shared_buffers.h"
33 #include "goto2graph.h"
34 
37  value_setst &value_sets,
38  symbol_tablet &symbol_table,
39  const irep_idt &function,
40  goto_programt &goto_program,
41 #ifdef LOCAL_MAY
42  const goto_functionst::goto_functiont &goto_function,
43 #endif
44  messaget &message)
45 {
46  namespacet ns(symbol_table);
47  unsigned tmp_counter=0;
48 
49 #ifdef LOCAL_MAY
50  local_may_aliast local_may(goto_function);
51 #endif
52 
53  Forall_goto_program_instructions(i_it, goto_program)
54  {
55  goto_programt::instructiont &instruction=*i_it;
56 
57  message.debug() <<instruction.source_location<< messaget::eom;
58 
59  if(instruction.is_goto() ||
60  instruction.is_assert() ||
61  instruction.is_assume())
62  {
63  rw_set_loct rw_set(ns, value_sets, i_it
64 #ifdef LOCAL_MAY
65  , local_may
66 #endif
67  ); // NOLINT(whitespace/parens)
68  if(rw_set.empty())
69  continue;
70 
71  symbolt new_symbol;
72  new_symbol.base_name="$tmp_guard";
73  new_symbol.name=
74  id2string(function)+"$tmp_guard"+std::to_string(tmp_counter++);
75  new_symbol.type=bool_typet();
76  new_symbol.is_static_lifetime=true;
77  new_symbol.is_thread_local=true;
78  new_symbol.value.make_nil();
79 
80  symbol_exprt symbol_expr=new_symbol.symbol_expr();
81 
82  symbolt *symbol_ptr;
83  symbol_table.move(new_symbol, symbol_ptr);
84 
86  new_i.make_assignment();
87  new_i.code=code_assignt(symbol_expr, instruction.guard);
88  new_i.source_location=instruction.source_location;
89  new_i.function=instruction.function;
90 
91  // replace guard
92  instruction.guard=symbol_expr;
93  goto_program.insert_before_swap(i_it, new_i);
94 
95  i_it++; // step forward
96  }
97  else if(instruction.is_function_call())
98  {
99  // nothing
100  }
101  }
102 }
103 
105  memory_modelt model,
106  value_setst &value_sets,
107  goto_modelt &goto_model,
108  bool SCC,
109  instrumentation_strategyt event_strategy,
110  bool no_cfg_kill,
111  bool no_dependencies,
112  loop_strategyt duplicate_body,
113  unsigned input_max_var,
114  unsigned input_max_po_trans,
115  bool render_po,
116  bool render_file,
117  bool render_function,
118  bool cav11_option,
119  bool hide_internals,
120  message_handlert &message_handler,
121  bool ignore_arrays)
122 {
123  messaget message(message_handler);
124 
125  // no more used -- dereferences performed in rw_set
126  // get rid of pointers
127  // remove_pointers(goto_functions, symbol_table, value_sets);
128  // add_failed_symbols(symbol_table);
129  // message.status() <<"pointers removed"<< messaget::eom;
130 
131  message.status() << "--------" << messaget::eom;
132 
133  // all access to shared variables is pushed into assignments
134  Forall_goto_functions(f_it, goto_model.goto_functions)
135  if(f_it->first != INITIALIZE_FUNCTION &&
136  f_it->first!=goto_functionst::entry_point())
137  introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first,
138  f_it->second.body,
139 #ifdef LOCAL_MAY
140  f_it->second,
141 #endif
142  message);
143 
144  message.status() << "Temp added" << messaget::eom;
145 
146  unsigned max_thds = 0;
147  instrumentert instrumenter(goto_model, message);
148  max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies,
149  duplicate_body);
150  message.status()<<"abstraction completed"<<messaget::eom;
151 
152  // collects cycles, directly or by SCCs
153  if(input_max_var!=0 || input_max_po_trans!=0)
154  instrumenter.set_parameters_collection(input_max_var,
155  input_max_po_trans, ignore_arrays);
156  else
157  instrumenter.set_parameters_collection(max_thds, 0, ignore_arrays);
158 
159  if(SCC)
160  {
161  instrumenter.collect_cycles_by_SCCs(model);
162  message.status()<<"cycles collected: "<<messaget::eom;
163  unsigned interesting_scc = 0;
164  unsigned total_cycles = 0;
165  for(unsigned i=0; i<instrumenter.num_sccs; i++)
166  if(instrumenter.egraph_SCCs[i].size()>=4)
167  {
168  message.status()<<"SCC #"<<i<<": "
169  <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
170  <<" cycles found"<<messaget::eom;
171  total_cycles += instrumenter
172  .set_of_cycles_per_SCC[interesting_scc++].size();
173  }
174 
175  /* if no cycle, no need to instrument */
176  if(total_cycles == 0)
177  {
178  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
179  return;
180  }
181  }
182  else
183  {
184  instrumenter.collect_cycles(model);
185  message.status()<<"cycles collected: "<<instrumenter.set_of_cycles.size()
186  <<" cycles found"<<messaget::eom;
187 
188  /* if no cycle, no need to instrument */
189  if(instrumenter.set_of_cycles.empty())
190  {
191  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
192  return;
193  }
194  }
195 
196  if(!no_cfg_kill)
197  instrumenter.cfg_cycles_filter();
198 
199  // collects instructions to instrument, depending on the strategy selected
200  if(event_strategy == my_events)
201  {
202  const std::set<event_idt> events_set = instrumentert::extract_my_events();
203  instrumenter.instrument_my_events(events_set);
204  }
205  else
206  instrumenter.instrument_with_strategy(event_strategy);
207 
208  // prints outputs
209  instrumenter.set_rendering_options(render_po, render_file, render_function);
210  instrumenter.print_outputs(model, hide_internals);
211 
212  // now adds buffers
213  shared_bufferst shared_buffers(
214  goto_model.symbol_table, max_thds, message);
215 
216  if(cav11_option)
217  shared_buffers.set_cav11(model);
218 
219  // stores the events to instrument
220  shared_buffers.cycles = instrumenter.var_to_instr; // var in the cycles
221  shared_buffers.cycles_loc = instrumenter.id2loc; // instrumented places
222  shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles
223 
224  // for reads delays
225  shared_buffers.affected_by_delay(value_sets, goto_model.goto_functions);
226 
227  for(std::set<irep_idt>::iterator it=
228  shared_buffers.affected_by_delay_set.begin();
229  it!=shared_buffers.affected_by_delay_set.end();
230  it++)
231  message.debug()<<id2string(*it)<<messaget::eom;
232 
233  message.status()<<"I instrument:"<<messaget::eom;
234  for(std::set<irep_idt>::iterator it=shared_buffers.cycles.begin();
235  it!=shared_buffers.cycles.end(); it++)
236  {
237  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
238  const std::pair<m_itt, m_itt> ran=
239  shared_buffers.cycles_loc.equal_range(*it);
240  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
241  message.result() << ((*it)==""?"fence":*it) << ", "
242  << ran_it->second << messaget::eom;
243  }
244 
246  shared_buffers, goto_model.symbol_table, goto_model.goto_functions);
247  visitor.weak_memory(
248  value_sets, goto_model.goto_functions.entry_point(), model);
249 
250  /* removes potential skips */
251  remove_skip(goto_model);
252 
253  // initialization code for buffers
254  shared_buffers.add_initialization_code(goto_model.goto_functions);
255 
256  // update counters etc.
257  goto_model.goto_functions.update();
258 
259  message.status()<< "Goto-program instrumented" << messaget::eom;
260 }
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:87
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
void add_initialization_code(goto_functionst &goto_functions)
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
bool is_thread_local
Definition: symbol.h:65
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:330
instrumentation_strategyt
Definition: wmm.h:26
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:36
bool empty() const
Definition: rw_set.h:72
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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:34
The Boolean type.
Definition: std_types.h:28
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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:358
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:391
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
memory_modelt
Definition: wmm.h:17
void instrument_my_events(const std::set< event_idt > &events)
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
std::multimap< irep_idt, source_locationt > cycles_r_loc
unsigned num_sccs
Definition: goto2graph.h:296
Instrumenter.
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
#define INITIALIZE_FUNCTION
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:331
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:93
::goto_functiont goto_functiont
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:332
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
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:35
void cfg_cycles_filter()
std::multimap< irep_idt, source_locationt > cycles_loc
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static eomt eom
Definition: message.h:285
Definition: wmm.h:32
typet type
Type of symbol.
Definition: symbol.h:31
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mstreamt & status() const
Definition: message.h:402
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
static std::set< event_idt > extract_my_events()
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#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:312
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:292
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:371
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:154
std::set< irep_idt > affected_by_delay_set
Program Transformation.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:289
A codet representing an assignment in the program.
Definition: std_code.h:256
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:295
Race Detection for Threaded Goto Programs.