CBMC
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,
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
107 ,
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,
120 value_setst &value_sets
122 ,
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
138 ,
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,
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 */
164 value_setst &value_sets
166 ,
168#endif
169 ); // NOLINT(whitespace/parens)
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<
193 std::set<nodet>,
196
198 std::set<goto_programt::const_targett, goto_programt::target_less_than>
200
201 /* "next nodes" (bwd steps in fwd/bck analysis) */
203
204 #define add_all_pos(it, target, source) \
205 for(std::set<nodet>::const_iterator \
206 it=(source).begin(); \
207 it!=(source).end(); ++it) \
208 (target).insert(*it);
209
210 #ifdef CONTEXT_INSENSITIVE
211 /* to keep track of the functions (and their start/end nodes) */
212 std::stack<irep_idt> stack_fun;
214 std::map<irep_idt, std::set<nodet> > in_nodes, out_nodes;
215 #endif
216
217 /* current thread number */
218 unsigned thread;
219
220 /* dependencies */
222
223 /* writes and reads to unknown addresses -- conservative */
224 std::set<event_idt> unknown_read_nodes;
225 std::set<event_idt> unknown_write_nodes;
226
227 /* set of functions visited so far -- we don't handle recursive functions */
228 std::set<irep_idt> functions_met;
229
244
245 void inline enter_function(const irep_idt &function_id)
246 {
247 if(functions_met.find(function_id) != functions_met.end())
248 throw "sorry, doesn't handle recursive function for the moment";
249 functions_met.insert(function_id);
250 }
251
252 void inline leave_function(const irep_idt &function_id)
253 {
254 functions_met.erase(function_id);
255 }
256
257 void inline visit_cfg(
258 value_setst &value_sets,
259 memory_modelt model,
260 bool no_dependencies,
262 const irep_idt &function_id)
263 {
264 /* ignore recursive calls -- underapproximation */
265 try
266 {
267 /* forbids recursive function */
268 enter_function(function_id);
269 std::set<nodet> end_out;
271 value_sets,
272 model,
275 function_id,
276 end_out);
277 leave_function(function_id);
278 }
279 catch(const std::string &s)
280 {
282 }
283 }
284
293 virtual void visit_cfg_function(
294 value_setst &value_sets,
295 memory_modelt model,
296 bool no_dependencies,
298 const irep_idt &function_id,
299 std::set<nodet> &ending_vertex);
300
301 bool inline local(const irep_idt &i);
302 };
303
304public:
305 /* message */
307
308 /* graph */
310
311 /* graph split into strongly connected components */
312 std::vector<std::set<event_idt> > egraph_SCCs;
313
314 /* critical cycles */
315 std::set<event_grapht::critical_cyclet> set_of_cycles;
316
317 /* critical cycles per SCC */
318 std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
319 unsigned num_sccs;
320
321 /* map from function to begin and end of the corresponding part of the
322 graph */
323 typedef std::map<irep_idt, std::pair<std::set<event_idt>,
324 std::set<event_idt> > > map_function_nodest;
326
328 {
329 for(map_function_nodest::const_iterator it=map_function_graph.begin();
330 it!=map_function_graph.end();
331 ++it)
332 {
333 message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
334 message.debug() << "Start nodes: ";
335 for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
336 in_it!=it->second.first.end();
337 ++in_it)
338 message.debug() << *in_it << " ";
340 message.debug() << "End nodes: ";
341 for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
342 in_it!=it->second.second.end();
343 ++in_it)
344 message.debug() << *in_it << " ";
346 }
347 }
348
349 /* variables to instrument, locations of variables to instrument on
350 the cycles, and locations of all the variables on the critical cycles */
351 /* TODO: those maps are here to interface easily with weak_mem.cpp,
352 but a rewriting of weak_mem can eliminate them */
353 std::set<irep_idt> var_to_instr;
354 std::multimap<irep_idt, source_locationt> id2loc;
355 std::multimap<irep_idt, source_locationt> id2cycloc;
356
370
371 /* abstracts goto-programs in abstract event graph, and computes
372 the thread numbering and returns the max number */
373 unsigned goto2graph_cfg(
374 value_setst &value_sets,
375 memory_modelt model,
376 bool no_dependencies,
377 /* forces the duplication, with arrays or not; otherwise, arrays only */
379
380 /* collects directly all the cycles in the graph */
382 {
384 num_sccs = 0;
385 }
386
387 /* collects the cycles in the graph by SCCs */
389
390 /* filters cycles spurious by CFG */
391 void cfg_cycles_filter();
392
393 /* sets parameters for collection, if required */
395 unsigned _max_var = 0,
396 unsigned _max_po_trans = 0,
397 bool _ignore_arrays = false)
398 {
400 }
401
402 /* builds the relations between unsafe pairs in the critical cycles and
403 instructions to instrument in the code */
404
405 /* strategies for instrumentation */
407 void instrument_my_events(const std::set<event_idt> &events);
408
409 /* retrieves events to filter in the instrumentation choice
410 with option --my-events */
411 static std::set<event_idt> extract_my_events();
412
413 /* sets rendering options */
414 void set_rendering_options(bool aligned, bool file, bool function)
415 {
416 PRECONDITION(!file || !function);
417 render_po_aligned = aligned;
418 render_by_file = file;
419 render_by_function = function;
420 }
421
422 /* prints outputs:
423 - cycles.dot: graph of the instrumented cycles
424 - ref.txt: names of the instrumented cycles
425 - output.txt: names of the instructions in the code
426 - all.txt: all */
427 void print_outputs(memory_modelt model, bool hide_internals);
428};
429
430#endif // CPROVER_GOTO_INSTRUMENT_WMM_GOTO2GRAPH_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:228
std::set< event_idt > unknown_read_nodes
Definition goto2graph.h:224
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:225
instrumentert & instrumenter
Definition goto2graph.h:90
void leave_function(const irep_idt &function_id)
Definition goto2graph.h:252
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::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::map< goto_programt::const_targett, std::set< nodet >, goto_programt::target_less_than > incoming_post
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:257
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:245
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:230
std::set< goto_programt::const_targett, goto_programt::target_less_than > updated
Definition goto2graph.h:199
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:355
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:357
unsigned num_sccs
Definition goto2graph.h:319
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:309
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:315
void collect_cycles(memory_modelt model)
Definition goto2graph.h:381
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:353
std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Definition goto2graph.h:324
std::vector< std::set< event_idt > > egraph_SCCs
Definition goto2graph.h:312
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition goto2graph.h:394
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
std::multimap< irep_idt, source_locationt > id2loc
Definition goto2graph.h:354
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:325
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:318
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:306
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:414
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:327
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
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:359
graph of abstract events
Symbol Table + CFG.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
A total order over targett and const_targett.
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