cprover
weak_memory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Weak Memory Instrumentation for Threaded Goto Programs
4
5Author: Daniel Kroening, Vincent Nimal
6
7Date: 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
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
46 messaget &message)
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 for(auto &gf_entry : goto_model.goto_functions.function_map)
138 {
139 if(
140 gf_entry.first != INITIALIZE_FUNCTION &&
141 gf_entry.first != goto_functionst::entry_point())
142 {
144 value_sets,
145 goto_model.symbol_table,
146 gf_entry.first,
147 gf_entry.second.body,
148#ifdef LOCAL_MAY
149 gf_entry.second,
150#endif
151 message);
152 }
153 }
154
155 message.status() << "Temp added" << messaget::eom;
156
157 unsigned max_thds = 0;
158 instrumentert instrumenter(goto_model, message);
159 max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies,
160 duplicate_body);
161 message.status()<<"abstraction completed"<<messaget::eom;
162
163 // collects cycles, directly or by SCCs
164 if(input_max_var!=0 || input_max_po_trans!=0)
165 instrumenter.set_parameters_collection(input_max_var,
166 input_max_po_trans, ignore_arrays);
167 else
168 instrumenter.set_parameters_collection(max_thds, 0, ignore_arrays);
169
170 if(SCC)
171 {
172 instrumenter.collect_cycles_by_SCCs(model);
173 message.status()<<"cycles collected: "<<messaget::eom;
174 unsigned interesting_scc = 0;
175 unsigned total_cycles = 0;
176 for(unsigned i=0; i<instrumenter.num_sccs; i++)
177 if(instrumenter.egraph_SCCs[i].size()>=4)
178 {
179 message.status()<<"SCC #"<<i<<": "
180 <<instrumenter.set_of_cycles_per_SCC[interesting_scc++].size()
181 <<" cycles found"<<messaget::eom;
182 total_cycles += instrumenter
183 .set_of_cycles_per_SCC[interesting_scc++].size();
184 }
185
186 /* if no cycle, no need to instrument */
187 if(total_cycles == 0)
188 {
189 message.status()<<"program safe -- no need to instrument"<<messaget::eom;
190 return;
191 }
192 }
193 else
194 {
195 instrumenter.collect_cycles(model);
196 message.status()<<"cycles collected: "<<instrumenter.set_of_cycles.size()
197 <<" cycles found"<<messaget::eom;
198
199 /* if no cycle, no need to instrument */
200 if(instrumenter.set_of_cycles.empty())
201 {
202 message.status()<<"program safe -- no need to instrument"<<messaget::eom;
203 return;
204 }
205 }
206
207 if(!no_cfg_kill)
208 instrumenter.cfg_cycles_filter();
209
210 // collects instructions to instrument, depending on the strategy selected
211 if(event_strategy == my_events)
212 {
213 const std::set<event_idt> events_set = instrumentert::extract_my_events();
214 instrumenter.instrument_my_events(events_set);
215 }
216 else
217 instrumenter.instrument_with_strategy(event_strategy);
218
219 // prints outputs
220 instrumenter.set_rendering_options(render_po, render_file, render_function);
221 instrumenter.print_outputs(model, hide_internals);
222
223 // now adds buffers
224 shared_bufferst shared_buffers(
225 goto_model.symbol_table, max_thds, message);
226
227 if(cav11_option)
228 shared_buffers.set_cav11(model);
229
230 // stores the events to instrument
231 shared_buffers.cycles = instrumenter.var_to_instr; // var in the cycles
232 shared_buffers.cycles_loc = instrumenter.id2loc; // instrumented places
233 shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles
234
235 // for reads delays
236 shared_buffers.affected_by_delay(value_sets, goto_model.goto_functions);
237
238 for(std::set<irep_idt>::iterator it=
239 shared_buffers.affected_by_delay_set.begin();
240 it!=shared_buffers.affected_by_delay_set.end();
241 it++)
242 message.debug()<<id2string(*it)<<messaget::eom;
243
244 message.status()<<"I instrument:"<<messaget::eom;
245 for(std::set<irep_idt>::iterator it=shared_buffers.cycles.begin();
246 it!=shared_buffers.cycles.end(); it++)
247 {
248 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
249 const std::pair<m_itt, m_itt> ran=
250 shared_buffers.cycles_loc.equal_range(*it);
251 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
252 message.result() << (it->empty() ? "fence" : *it) << ", "
253 << ran_it->second << messaget::eom;
254 }
255
257 shared_buffers, goto_model.symbol_table, goto_model.goto_functions);
258 visitor.weak_memory(
259 value_sets, goto_model.goto_functions.entry_point(), model);
260
261 /* removes potential skips */
262 remove_skip(goto_model);
263
264 // initialization code for buffers
265 shared_buffers.add_initialization_code(goto_model.goto_functions);
266
267 // update counters etc.
268 goto_model.goto_functions.update();
269
270 message.status()<< "Goto-program instrumented" << messaget::eom;
271}
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:375
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:351
void print_outputs(memory_modelt model, bool hide_internals)
unsigned num_sccs
Definition: goto2graph.h:315
void instrument_my_events(const std::set< event_idt > &events)
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:311
void collect_cycles(memory_modelt model)
Definition: goto2graph.h:377
void instrument_with_strategy(instrumentation_strategyt strategy)
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:349
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:308
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:390
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:350
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:314
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 cfg_cycles_filter()
void set_rendering_options(bool aligned, bool file, bool function)
Definition: goto2graph.h:410
static std::set< event_idt > extract_my_events()
void make_nil()
Definition: irep.h:454
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & debug() const
Definition: message.h:429
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
bool empty() const
Definition: rw_set.h:74
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
std::multimap< irep_idt, source_locationt > cycles_loc
void set_cav11(memory_modelt model)
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...
std::set< irep_idt > affected_by_delay_set
std::set< irep_idt > cycles
std::multimap< irep_idt, source_locationt > cycles_r_loc
void add_initialization_code(goto_functionst &goto_functions)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
bool is_thread_local
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
exprt value
Initial value of symbol.
Definition: symbol.h:34
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Instrumenter.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
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)
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
Weak Memory Instrumentation for Threaded Goto Programs.
memory_modelt
Definition: wmm.h:18
loop_strategyt
Definition: wmm.h:37
instrumentation_strategyt
Definition: wmm.h:27
@ my_events
Definition: wmm.h:32