cprover
cfg.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Control Flow Graph
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_CFG_H
13 #define CPROVER_GOTO_PROGRAMS_CFG_H
14 
15 #include <util/std_expr.h>
16 #include <util/graph.h>
17 
18 #include "goto_functions.h"
19 
21 {
22 };
23 
24 // these are the CFG nodes
25 template<class T, typename I>
26 struct cfg_base_nodet:public graph_nodet<empty_edget>, public T
27 {
30 
31  I PC;
32 };
33 
59 template<class T,
60  typename P=const goto_programt,
62 class cfg_baset:public grapht< cfg_base_nodet<T, I> >
63 {
64 public:
65  typedef std::size_t entryt;
66 
67  struct entry_mapt:
68  public std::map<goto_programt::const_targett, entryt>
69  {
71 
72  explicit entry_mapt(grapht< cfg_base_nodet<T, I> > &_container):
73  container(_container)
74  {
75  }
76 
78  {
79  std::pair<iterator, bool> e=insert(std::make_pair(t, 0));
80 
81  if(e.second)
82  e.first->second=container.add_node();
83 
84  return e.first->second;
85  }
86  };
87  entry_mapt entry_map;
88 
89 protected:
90  virtual void compute_edges_goto(
91  const goto_programt &goto_program,
92  const goto_programt::instructiont &instruction,
94  entryt &entry);
95 
96  virtual void compute_edges_catch(
97  const goto_programt &goto_program,
98  const goto_programt::instructiont &instruction,
100  entryt &entry);
101 
102  virtual void compute_edges_throw(
103  const goto_programt &goto_program,
104  const goto_programt::instructiont &instruction,
106  entryt &entry);
107 
108  virtual void compute_edges_start_thread(
109  const goto_programt &goto_program,
110  const goto_programt::instructiont &instruction,
112  entryt &entry);
113 
114  virtual void compute_edges_function_call(
115  const goto_functionst &goto_functions,
116  const goto_programt &goto_program,
117  const goto_programt::instructiont &instruction,
119  entryt &entry);
120 
121  void compute_edges(
122  const goto_functionst &goto_functions,
123  const goto_programt &goto_program,
124  I PC);
125 
126  void compute_edges(
127  const goto_functionst &goto_functions,
128  P &goto_program);
129 
130  void compute_edges(
131  const goto_functionst &goto_functions);
132 
133 public:
134  cfg_baset():entry_map(*this)
135  {
136  }
137 
138  virtual ~cfg_baset()
139  {
140  }
141 
143  const goto_functionst &goto_functions)
144  {
145  compute_edges(goto_functions);
146  }
147 
148  void operator()(P &goto_program)
149  {
150  goto_functionst goto_functions;
151  compute_edges(goto_functions, goto_program);
152  }
153 
154  I get_first_node(P &program) const { return program.instructions.begin(); }
155  I get_last_node(P &program) const { return --program.instructions.end(); }
156  bool nodes_empty(P &program) const { return program.instructions.empty(); }
157 };
158 
159 template<class T,
160  typename P=const goto_programt,
161  typename I=goto_programt::const_targett>
162 class concurrent_cfg_baset:public virtual cfg_baset<T, P, I>
163 {
164 protected:
165  virtual void compute_edges_start_thread(
166  const goto_programt &goto_program,
167  const goto_programt::instructiont &instruction,
169  typename cfg_baset<T, P, I>::entryt &entry);
170 };
171 
172 template<class T,
173  typename P=const goto_programt,
174  typename I=goto_programt::const_targett>
175 class procedure_local_cfg_baset:public virtual cfg_baset<T, P, I>
176 {
177 protected:
178  virtual void compute_edges_function_call(
179  const goto_functionst &goto_functions,
180  const goto_programt &goto_program,
181  const goto_programt::instructiont &instruction,
183  typename cfg_baset<T, P, I>::entryt &entry);
184 };
185 
186 template<class T,
187  typename P=const goto_programt,
188  typename I=goto_programt::const_targett>
190  public concurrent_cfg_baset<T, P, I>,
191  public procedure_local_cfg_baset<T, P, I>
192 {
193 };
194 
195 template<class T, typename P, typename I>
197  const goto_programt &goto_program,
198  const goto_programt::instructiont &instruction,
200  entryt &entry)
201 {
202  if(next_PC!=goto_program.instructions.end() &&
203  !instruction.guard.is_true())
204  this->add_edge(entry, entry_map[next_PC]);
205 
206  for(const auto &t : instruction.targets)
207  if(t!=goto_program.instructions.end())
208  this->add_edge(entry, entry_map[t]);
209 }
210 
211 template<class T, typename P, typename I>
213  const goto_programt &goto_program,
214  const goto_programt::instructiont &instruction,
216  entryt &entry)
217 {
218  if(next_PC!=goto_program.instructions.end())
219  this->add_edge(entry, entry_map[next_PC]);
220 
221  // Not ideal, but preserves targets
222  // Ideally, the throw statements should have those as successors
223 
224  for(const auto &t : instruction.targets)
225  if(t!=goto_program.instructions.end())
226  this->add_edge(entry, entry_map[t]);
227 }
228 
229 template<class T, typename P, typename I>
231  const goto_programt &goto_program,
232  const goto_programt::instructiont &instruction,
234  entryt &entry)
235 {
236  // no (trivial) successors
237 }
238 
239 template<class T, typename P, typename I>
241  const goto_programt &goto_program,
242  const goto_programt::instructiont &instruction,
244  entryt &entry)
245 {
246  if(next_PC!=goto_program.instructions.end())
247  this->add_edge(entry, entry_map[next_PC]);
248 }
249 
250 template<class T, typename P, typename I>
252  const goto_programt &goto_program,
253  const goto_programt::instructiont &instruction,
255  typename cfg_baset<T, P, I>::entryt &entry)
256 {
258  goto_program,
259  instruction,
260  next_PC,
261  entry);
262 
263  for(const auto &t : instruction.targets)
264  if(t!=goto_program.instructions.end())
265  this->add_edge(entry, this->entry_map[t]);
266 }
267 
268 template<class T, typename P, typename I>
270  const goto_functionst &goto_functions,
271  const goto_programt &goto_program,
272  const goto_programt::instructiont &instruction,
274  entryt &entry)
275 {
276  const exprt &function=
277  to_code_function_call(instruction.code).function();
278 
279  if(function.id()!=ID_symbol)
280  return;
281 
282  const irep_idt &identifier=
283  to_symbol_expr(function).get_identifier();
284 
285  goto_functionst::function_mapt::const_iterator f_it=
286  goto_functions.function_map.find(identifier);
287 
288  if(f_it!=goto_functions.function_map.end() &&
289  f_it->second.body_available())
290  {
291  // get the first instruction
293  f_it->second.body.instructions.begin();
294 
296  f_it->second.body.instructions.end();
297 
298  goto_programt::const_targett last_it=e_it; last_it--;
299 
300  if(i_it!=e_it)
301  {
302  // nonempty function
303  this->add_edge(entry, entry_map[i_it]);
304 
305  // add the last instruction as predecessor of the return location
306  if(next_PC!=goto_program.instructions.end())
307  this->add_edge(entry_map[last_it], entry_map[next_PC]);
308  }
309  else if(next_PC!=goto_program.instructions.end())
310  {
311  // empty function
312  this->add_edge(entry, entry_map[next_PC]);
313  }
314  }
315  else if(next_PC!=goto_program.instructions.end())
316  this->add_edge(entry, entry_map[next_PC]);
317 }
318 
319 template<class T, typename P, typename I>
321  const goto_functionst &goto_functions,
322  const goto_programt &goto_program,
323  const goto_programt::instructiont &instruction,
325  typename cfg_baset<T, P, I>::entryt &entry)
326 {
327  const exprt &function=
328  to_code_function_call(instruction.code).function();
329 
330  if(function.id()!=ID_symbol)
331  return;
332 
333  if(next_PC!=goto_program.instructions.end())
334  this->add_edge(entry, this->entry_map[next_PC]);
335 }
336 
337 template<class T, typename P, typename I>
339  const goto_functionst &goto_functions,
340  const goto_programt &goto_program,
341  I PC)
342 {
343  const goto_programt::instructiont &instruction=*PC;
344  entryt entry=entry_map[PC];
345  (*this)[entry].PC=PC;
346  goto_programt::const_targett next_PC(PC);
347  next_PC++;
348 
349  // compute forward edges first
350  switch(instruction.type)
351  {
352  case GOTO:
353  compute_edges_goto(goto_program, instruction, next_PC, entry);
354  break;
355 
356  case CATCH:
357  compute_edges_catch(goto_program, instruction, next_PC, entry);
358  break;
359 
360  case THROW:
361  compute_edges_throw(goto_program, instruction, next_PC, entry);
362  break;
363 
364  case START_THREAD:
365  compute_edges_start_thread(
366  goto_program,
367  instruction,
368  next_PC,
369  entry);
370  break;
371 
372  case FUNCTION_CALL:
373  compute_edges_function_call(
374  goto_functions,
375  goto_program,
376  instruction,
377  next_PC,
378  entry);
379  break;
380 
381  case END_THREAD:
382  case END_FUNCTION:
383  // no successor
384  break;
385 
386  case ASSUME:
387  // false guard -> no successor
388  if(instruction.guard.is_false())
389  break;
390 
391  case ASSIGN:
392  case ASSERT:
393  case OTHER:
394  case RETURN:
395  case SKIP:
396  case LOCATION:
397  case ATOMIC_BEGIN:
398  case ATOMIC_END:
399  case DECL:
400  case DEAD:
401  if(next_PC!=goto_program.instructions.end())
402  this->add_edge(entry, entry_map[next_PC]);
403  break;
404 
405  case NO_INSTRUCTION_TYPE:
406  assert(false);
407  break;
408  }
409 }
410 
411 template<class T, typename P, typename I>
413  const goto_functionst &goto_functions,
414  P &goto_program)
415 {
416  for(I it=goto_program.instructions.begin();
417  it!=goto_program.instructions.end();
418  ++it)
419  compute_edges(goto_functions, goto_program, it);
420 }
421 
422 template<class T, typename P, typename I>
424  const goto_functionst &goto_functions)
425 {
426  forall_goto_functions(it, goto_functions)
427  if(it->second.body_available())
428  compute_edges(goto_functions, it->second.body);
429 }
430 
431 #endif // CPROVER_GOTO_PROGRAMS_CFG_H
I get_last_node(P &program) const
Definition: cfg.h:155
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
Definition: cfg.h:338
A generic directed graph with a parametric node type.
Definition: graph.h:132
entry_mapt entry_map
Definition: cfg.h:87
instructionst instructions
The list of instructions in the goto program.
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
Definition: cfg.h:62
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
virtual void compute_edges_goto(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
Definition: cfg.h:196
bool nodes_empty(P &program) const
Definition: cfg.h:156
std::size_t entryt
Definition: cfg.h:65
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
Definition: cfg.h:212
grapht< cfg_base_nodet< T, I > > & container
Definition: cfg.h:70
instructionst::const_iterator const_targett
void operator()(const goto_functionst &goto_functions)
Definition: cfg.h:142
API to expression classes.
graph_nodet< empty_edget >::edgest edgest
Definition: cfg.h:29
void operator()(P &goto_program)
Definition: cfg.h:148
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, typename cfg_baset< T, P, I >::entryt &entry)
Definition: cfg.h:251
virtual void compute_edges_function_call(const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, typename cfg_baset< T, P, I >::entryt &entry)
Definition: cfg.h:320
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
virtual void compute_edges_throw(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
Definition: cfg.h:230
A Template Class for Graphs.
node_indext add_node()
Definition: graph.h:145
graph_nodet< empty_edget >::edget edget
Definition: cfg.h:28
virtual ~cfg_baset()
Definition: cfg.h:138
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
cfg_baset()
Definition: cfg.h:134
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
I get_first_node(P &program) const
Definition: cfg.h:154
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
Definition: cfg.h:72
virtual void compute_edges_function_call(const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
Definition: cfg.h:269
#define forall_goto_functions(it, functions)
entryt & operator[](const goto_programt::const_targett &t)
Definition: cfg.h:77
This class represents a node in a directed graph.
Definition: graph.h:33
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
Definition: cfg.h:240
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700