cprover
Loading...
Searching...
No Matches
goto2graph.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrumenter
4
5Author: Vincent Nimal
6
7Date: 2012
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
15#define CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
16
17#include <map>
18
19#include <util/namespace.h>
20#include <util/message.h>
21
23
24#include "event_graph.h"
25#include "wmm.h"
26
27class value_setst;
28
30{
31public:
32 /* reference to goto-functions and symbol_table */
34
35protected:
37
38 /* alternative representation of graph (SCC) */
39 std::map<event_idt, event_idt> map_vertex_gnode;
41
42 unsigned unique_id;
43
44 /* rendering options */
48
49 bool inline local(const irep_idt &id);
50
51 void inline add_instr_to_interleaving(
52 goto_programt::instructionst::iterator it,
53 goto_programt &interleaving);
54
55 /* deprecated */
57
59
60 typedef std::set<event_grapht::critical_cyclet> set_of_cyclest;
61 void inline instrument_all_inserter(
62 const set_of_cyclest &set);
64 const set_of_cyclest &set);
66 const set_of_cyclest &set);
68 const set_of_cyclest &set);
70 const set_of_cyclest &set);
72 const set_of_cyclest &set, const std::set<event_idt> &events);
73
74 void inline print_outputs_local(
75 const std::set<event_grapht::critical_cyclet> &set,
76 std::ofstream &dot,
77 std::ofstream &ref,
78 std::ofstream &output,
79 std::ofstream &all,
80 std::ofstream &table,
81 memory_modelt model,
82 bool hide_internals);
83
84 typedef std::set<goto_programt::instructiont::targett> target_sett;
85
87 {
88 protected:
91
92 /* pointer to the egraph(s) that we construct */
94 std::vector<std::set<event_idt>> &egraph_SCCs;
96
97 /* for thread marking (dynamic) */
99 unsigned coming_from;
100
102 const irep_idt &function_id,
105 value_setst &value_sets
106#ifdef LOCAL_MAY
107 ,
108 local_may_aliast local_may
109#endif
110 ) const; // NOLINT(whitespace/parens)
111
112 /* transformers */
113 void visit_cfg_thread() const;
114 void visit_cfg_propagate(goto_programt::instructionst::iterator i_it);
115 void visit_cfg_body(
116 const irep_idt &function_id,
117 const goto_programt &goto_program,
119 loop_strategyt replicate_body,
120 value_setst &value_sets
121#ifdef LOCAL_MAY
122 ,
123 local_may_aliast &local_may
124#endif
125 ); // deprecated NOLINT(whitespace/parens)
128 void inline visit_cfg_duplicate(
129 const goto_programt &goto_program,
132 void visit_cfg_assign(
133 value_setst &value_sets,
134 const irep_idt &function_id,
135 goto_programt::instructionst::iterator &i_it,
136 bool no_dependencies
137#ifdef LOCAL_MAY
138 ,
139 local_may_aliast &local_may
140#endif
141 ); // NOLINT(whitespace/parens)
142 void visit_cfg_fence(
143 goto_programt::instructionst::iterator i_it,
144 const irep_idt &function_id);
145 void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
147 goto_programt::instructionst::iterator i_it,
148 const irep_idt &function_id);
150 goto_programt::instructionst::iterator i_it,
151 const irep_idt &function_id);
152 void visit_cfg_function_call(value_setst &value_sets,
153 goto_programt::instructionst::iterator i_it,
154 memory_modelt model,
155 bool no_dependenciess,
156 loop_strategyt duplicate_body);
157 void visit_cfg_goto(
158 const irep_idt &function_id,
159 const goto_programt &goto_program,
160 goto_programt::instructionst::iterator i_it,
161 /* forces the duplication of all the loops, with array or not
162 otherwise, duplication of loops with array accesses only */
163 loop_strategyt replicate_body,
164 value_setst &value_sets
165#ifdef LOCAL_MAY
166 ,
167 local_may_aliast &local_may
168#endif
169 ); // NOLINT(whitespace/parens)
170 void visit_cfg_reference_function(irep_idt id_function);
171
172 public:
174 {
175 }
176
177 unsigned max_thread;
178
179 /* relations between irep and Reads/Writes */
180 typedef std::multimap<irep_idt, event_idt> id2nodet;
181 typedef std::pair<irep_idt, event_idt> id2node_pairt;
183
185 unsigned read_counter;
186 unsigned ws_counter;
188
189 /* previous nodes (fwd analysis) */
190 typedef std::pair<event_idt, event_idt> nodet;
191 typedef std::map<goto_programt::const_targett, std::set<nodet> >
193
195 std::set<goto_programt::const_targett> updated;
196
197 /* "next nodes" (bwd steps in fwd/bck analysis) */
199
200 #define add_all_pos(it, target, source) \
201 for(std::set<nodet>::const_iterator \
202 it=(source).begin(); \
203 it!=(source).end(); ++it) \
204 (target).insert(*it);
205
206 #ifdef CONTEXT_INSENSITIVE
207 /* to keep track of the functions (and their start/end nodes) */
208 std::stack<irep_idt> stack_fun;
209 irep_idt cur_fun;
210 std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
211 #endif
212
213 /* current thread number */
214 unsigned thread;
215
216 /* dependencies */
218
219 /* writes and reads to unknown addresses -- conservative */
220 std::set<event_idt> unknown_read_nodes;
221 std::set<event_idt> unknown_write_nodes;
222
223 /* set of functions visited so far -- we don't handle recursive functions */
224 std::set<irep_idt> functions_met;
225
227 :ns(_ns), instrumenter(_instrumenter), egraph(_instrumenter.egraph),
228 egraph_SCCs(_instrumenter.egraph_SCCs),
229 egraph_alt(_instrumenter.egraph_alt)
230 {
231 write_counter = 0;
232 read_counter = 0;
233 ws_counter = 0;
234 fr_rf_counter = 0;
235 thread = 0;
236 current_thread = 0;
237 max_thread = 0;
238 coming_from = 0;
239 }
240
241 void inline enter_function(const irep_idt &function_id)
242 {
243 if(functions_met.find(function_id) != functions_met.end())
244 throw "sorry, doesn't handle recursive function for the moment";
245 functions_met.insert(function_id);
246 }
247
248 void inline leave_function(const irep_idt &function_id)
249 {
250 functions_met.erase(function_id);
251 }
252
253 void inline visit_cfg(
254 value_setst &value_sets,
255 memory_modelt model,
256 bool no_dependencies,
257 loop_strategyt duplicate_body,
258 const irep_idt &function_id)
259 {
260 /* ignore recursive calls -- underapproximation */
261 try
262 {
263 /* forbids recursive function */
264 enter_function(function_id);
265 std::set<nodet> end_out;
267 value_sets,
268 model,
269 no_dependencies,
270 duplicate_body,
271 function_id,
272 end_out);
273 leave_function(function_id);
274 }
275 catch(const std::string &s)
276 {
278 }
279 }
280
289 virtual void visit_cfg_function(
290 value_setst &value_sets,
291 memory_modelt model,
292 bool no_dependencies,
293 loop_strategyt duplicate_body,
294 const irep_idt &function_id,
295 std::set<nodet> &ending_vertex);
296
297 bool inline local(const irep_idt &i);
298 };
299
300public:
301 /* message */
303
304 /* graph */
306
307 /* graph split into strongly connected components */
308 std::vector<std::set<event_idt> > egraph_SCCs;
309
310 /* critical cycles */
311 std::set<event_grapht::critical_cyclet> set_of_cycles;
312
313 /* critical cycles per SCC */
314 std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
315 unsigned num_sccs;
316
317 /* map from function to begin and end of the corresponding part of the
318 graph */
319 typedef std::map<irep_idt, std::pair<std::set<event_idt>,
320 std::set<event_idt> > > map_function_nodest;
322
324 {
325 for(map_function_nodest::const_iterator it=map_function_graph.begin();
326 it!=map_function_graph.end();
327 ++it)
328 {
329 message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
330 message.debug() << "Start nodes: ";
331 for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
332 in_it!=it->second.first.end();
333 ++in_it)
334 message.debug() << *in_it << " ";
336 message.debug() << "End nodes: ";
337 for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
338 in_it!=it->second.second.end();
339 ++in_it)
340 message.debug() << *in_it << " ";
342 }
343 }
344
345 /* variables to instrument, locations of variables to instrument on
346 the cycles, and locations of all the variables on the critical cycles */
347 /* TODO: those maps are here to interface easily with weak_mem.cpp,
348 but a rewriting of weak_mem can eliminate them */
349 std::set<irep_idt> var_to_instr;
350 std::multimap<irep_idt, source_locationt> id2loc;
351 std::multimap<irep_idt, source_locationt> id2cycloc;
352
354 goto_modelt &_goto_model,
355 messaget &_message):
356 ns(_goto_model.symbol_table),
357 goto_functions(_goto_model.goto_functions),
358 render_po_aligned(true),
359 render_by_file(false),
360 render_by_function(false),
361 message(_message),
362 egraph(_message),
363 num_sccs(0)
364 {
365 }
366
367 /* abstracts goto-programs in abstract event graph, and computes
368 the thread numbering and returns the max number */
369 unsigned goto2graph_cfg(
370 value_setst &value_sets,
371 memory_modelt model,
372 bool no_dependencies,
373 /* forces the duplication, with arrays or not; otherwise, arrays only */
374 loop_strategyt duplicate_body);
375
376 /* collects directly all the cycles in the graph */
378 {
380 num_sccs = 0;
381 }
382
383 /* collects the cycles in the graph by SCCs */
385
386 /* filters cycles spurious by CFG */
387 void cfg_cycles_filter();
388
389 /* sets parameters for collection, if required */
391 unsigned _max_var = 0,
392 unsigned _max_po_trans = 0,
393 bool _ignore_arrays = false)
394 {
395 egraph.set_parameters_collection(_max_var, _max_po_trans, _ignore_arrays);
396 }
397
398 /* builds the relations between unsafe pairs in the critical cycles and
399 instructions to instrument in the code */
400
401 /* strategies for instrumentation */
403 void instrument_my_events(const std::set<event_idt> &events);
404
405 /* retrieves events to filter in the instrumentation choice
406 with option --my-events */
407 static std::set<event_idt> extract_my_events();
408
409 /* sets rendering options */
410 void set_rendering_options(bool aligned, bool file, bool function)
411 {
412 render_po_aligned = aligned;
414 render_by_function = function;
416 }
417
418 /* prints outputs:
419 - cycles.dot: graph of the instrumented cycles
420 - ref.txt: names of the instrumented cycles
421 - output.txt: names of the instructions in the code
422 - all.txt: all */
423 void print_outputs(memory_modelt model, bool hide_internals);
424};
425
426#endif // CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
std::set< irep_idt > functions_met
Definition goto2graph.h:224
std::set< event_idt > unknown_read_nodes
Definition goto2graph.h:220
bool contains_shared_array(const irep_idt &function_id, goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
std::set< event_idt > unknown_write_nodes
Definition goto2graph.h:221
instrumentert & instrumenter
Definition goto2graph.h:90
void leave_function(const irep_idt &function_id)
Definition goto2graph.h:248
virtual void visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
Definition goto2graph.h:192
std::pair< irep_idt, event_idt > id2node_pairt
Definition goto2graph.h:181
bool local(const irep_idt &i)
void visit_cfg_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
void visit_cfg_goto(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
void visit_cfg_function_call(value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body)
std::multimap< irep_idt, event_idt > id2nodet
Definition goto2graph.h:180
std::set< goto_programt::const_targett > updated
Definition goto2graph.h:195
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
std::vector< std::set< event_idt > > & egraph_SCCs
Definition goto2graph.h:94
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
void visit_cfg_assign(value_setst &value_sets, const irep_idt &function_id, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id)
Definition goto2graph.h:253
void visit_cfg_duplicate(const goto_programt &goto_program, goto_programt::const_targett targ, goto_programt::const_targett i_it)
void enter_function(const irep_idt &function_id)
Definition goto2graph.h:241
void visit_cfg_body(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
std::pair< event_idt, event_idt > nodet
Definition goto2graph.h:190
cfg_visitort(namespacet &_ns, instrumentert &_instrumenter)
Definition goto2graph.h:226
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
std::multimap< irep_idt, source_locationt > id2cycloc
Definition goto2graph.h:351
void print_outputs(memory_modelt model, bool hide_internals)
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
instrumentert(goto_modelt &_goto_model, messaget &_message)
Definition goto2graph.h:353
unsigned num_sccs
Definition goto2graph.h:315
void instrument_my_events(const std::set< event_idt > &events)
void instrument_all_inserter(const set_of_cyclest &set)
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
event_grapht egraph
Definition goto2graph.h:305
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
std::set< event_grapht::critical_cyclet > set_of_cyclest
Definition goto2graph.h:60
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition goto2graph.h:311
void collect_cycles(memory_modelt model)
Definition goto2graph.h:377
bool render_po_aligned
Definition goto2graph.h:45
void instrument_with_strategy(instrumentation_strategyt strategy)
std::set< irep_idt > var_to_instr
Definition goto2graph.h:349
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition goto2graph.h:320
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
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
std::multimap< irep_idt, source_locationt > id2loc
Definition goto2graph.h:350
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
bool render_by_function
Definition goto2graph.h:47
map_function_nodest map_function_graph
Definition goto2graph.h:321
goto_functionst & goto_functions
Definition goto2graph.h:36
bool render_by_file
Definition goto2graph.h:46
std::map< event_idt, event_idt > map_vertex_gnode
Definition goto2graph.h:39
void instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)
std::set< goto_programt::instructiont::targett > target_sett
Definition goto2graph.h:84
namespacet ns
Definition goto2graph.h:33
unsigned unique_id
Definition goto2graph.h:42
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition goto2graph.h:314
wmm_grapht egraph_alt
Definition goto2graph.h:40
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
messaget & message
Definition goto2graph.h:302
bool local(const irep_idt &id)
is local variable?
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...
void cfg_cycles_filter()
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
void set_rendering_options(bool aligned, bool file, bool function)
Definition goto2graph.h:410
static std::set< event_idt > extract_my_events()
void print_outputs_local(const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)
void print_map_function_graph() const
Definition goto2graph.h:323
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void dot(const goto_modelt &src, std::ostream &out)
Definition dot.cpp:353
graph of abstract events
Symbol Table + CFG.
Definition kdev_t.h:19
memory models
memory_modelt
Definition wmm.h:18
loop_strategyt
Definition wmm.h:37
instrumentation_strategyt
Definition wmm.h:27
@ all
Definition wmm.h:28