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,
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 
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  unsigned unwinding_bound,
111  bool no_cfg_kill,
112  bool no_dependencies,
113  loop_strategyt duplicate_body,
114  unsigned input_max_var,
115  unsigned input_max_po_trans,
116  bool render_po,
117  bool render_file,
118  bool render_function,
119  bool cav11_option,
120  bool hide_internals,
122  bool ignore_arrays)
123 {
124  messaget message(message_handler);
125 
126  // no more used -- dereferences performed in rw_set
127  // get rid of pointers
128  // remove_pointers(goto_functions, symbol_table, value_sets);
129  // add_failed_symbols(symbol_table);
130  // message.status() <<"pointers removed"<< messaget::eom;
131 
132  message.status() << "--------" << messaget::eom;
133 
134  // all access to shared variables is pushed into assignments
135  Forall_goto_functions(f_it, goto_model.goto_functions)
136  if(f_it->first != INITIALIZE_FUNCTION &&
137  f_it->first!=goto_functionst::entry_point())
138  introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first,
139  f_it->second.body,
140 #ifdef LOCAL_MAY
141  f_it->second,
142 #endif
143  message);
144 
145  message.status() << "Temp added" << messaget::eom;
146 
147  unsigned max_thds = 0;
148  instrumentert instrumenter(goto_model, message);
149  max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies,
150  duplicate_body);
151  message.status()<<"abstraction completed"<<messaget::eom;
152 
153  // collects cycles, directly or by SCCs
154  if(input_max_var!=0 || input_max_po_trans!=0)
155  instrumenter.set_parameters_collection(input_max_var,
156  input_max_po_trans, ignore_arrays);
157  else
158  instrumenter.set_parameters_collection(max_thds, ignore_arrays);
159 
160  if(SCC)
161  {
162  instrumenter.collect_cycles_by_SCCs(model);
163  message.status()<<"cycles collected: "<<messaget::eom;
164  unsigned interesting_scc = 0;
165  unsigned total_cycles = 0;
166  for(unsigned i=0; i<instrumenter.num_sccs; i++)
167  if(instrumenter.egraph_SCCs[i].size()>=4)
168  {
169  message.status()<<"SCC #"<<i<<": "
170  <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
171  <<" cycles found"<<messaget::eom;
172  total_cycles += instrumenter
173  .set_of_cycles_per_SCC[interesting_scc++].size();
174  }
175 
176  /* if no cycle, no need to instrument */
177  if(total_cycles == 0)
178  {
179  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
180  return;
181  }
182  }
183  else
184  {
185  instrumenter.collect_cycles(model);
186  message.status()<<"cycles collected: "<<instrumenter.set_of_cycles.size()
187  <<" cycles found"<<messaget::eom;
188 
189  /* if no cycle, no need to instrument */
190  if(instrumenter.set_of_cycles.empty())
191  {
192  message.status()<<"program safe -- no need to instrument"<<messaget::eom;
193  return;
194  }
195  }
196 
197  if(!no_cfg_kill)
198  instrumenter.cfg_cycles_filter();
199 
200  // collects instructions to instrument, depending on the strategy selected
201  if(event_strategy == my_events)
202  {
203  const std::set<event_idt> events_set = instrumentert::extract_my_events();
204  instrumenter.instrument_my_events(events_set);
205  }
206  else
207  instrumenter.instrument_with_strategy(event_strategy);
208 
209  // prints outputs
210  instrumenter.set_rendering_options(render_po, render_file, render_function);
211  instrumenter.print_outputs(model, hide_internals);
212 
213  // now adds buffers
214  shared_bufferst shared_buffers(
215  goto_model.symbol_table, max_thds, message);
216 
217  if(cav11_option)
218  shared_buffers.set_cav11(model);
219 
220  // stores the events to instrument
221  shared_buffers.cycles = instrumenter.var_to_instr; // var in the cycles
222  shared_buffers.cycles_loc = instrumenter.id2loc; // instrumented places
223  shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles
224 
225  // for reads delays
226  shared_buffers.affected_by_delay(
227  goto_model.symbol_table, value_sets, goto_model.goto_functions);
228 
229  for(std::set<irep_idt>::iterator it=
230  shared_buffers.affected_by_delay_set.begin();
231  it!=shared_buffers.affected_by_delay_set.end();
232  it++)
233  message.debug()<<id2string(*it)<<messaget::eom;
234 
235  message.status()<<"I instrument:"<<messaget::eom;
236  for(std::set<irep_idt>::iterator it=shared_buffers.cycles.begin();
237  it!=shared_buffers.cycles.end(); it++)
238  {
239  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
240  const std::pair<m_itt, m_itt> ran=
241  shared_buffers.cycles_loc.equal_range(*it);
242  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
243  message.result() << ((*it)==""?"fence":*it) << ", "
244  << ran_it->second << messaget::eom;
245  }
246 
248  shared_buffers, goto_model.symbol_table, goto_model.goto_functions);
249  visitor.weak_memory(
250  value_sets, goto_model.goto_functions.entry_point(), model);
251 
252  /* removes potential skips */
253  remove_skip(goto_model);
254 
255  // initialization code for buffers
256  shared_buffers.add_initialization_code(goto_model.goto_functions);
257 
258  // update counters etc.
259  goto_model.goto_functions.update();
260 
261  message.status()<< "Goto-program instrumented" << messaget::eom;
262 }
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:188
void add_initialization_code(goto_functionst &goto_functions)
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
bool is_thread_local
Definition: symbol.h:67
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:326
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
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, 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)
exprt value
Initial value of symbol.
Definition: symbol.h:37
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
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:67
void set_cav11(memory_modelt model)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:354
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:387
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
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...
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:292
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:327
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:328
void instrument_with_strategy(instrumentation_strategyt strategy)
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:70
Definition: wmm.h:32
typet type
Type of symbol.
Definition: symbol.h:34
static irep_idt entry_point()
mstreamt & status() const
Definition: message.h:317
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
static std::set< event_idt > extract_my_events()
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
std::set< irep_idt > cycles
void make_nil()
Definition: irep.h:243
goto_programt & goto_program
Definition: cover.cpp:63
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:288
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:367
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::set< irep_idt > affected_by_delay_set
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Program Transformation.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:285
Assignment.
Definition: std_code.h:195
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:291
Race Detection for Threaded Goto Programs.