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  class entry_mapt final
68  {
69  typedef std::map<goto_programt::const_targett, entryt> data_typet;
71 
72  public:
74 
75  // NOLINTNEXTLINE(readability/identifiers)
76  typedef data_typet::iterator iterator;
77  // NOLINTNEXTLINE(readability/identifiers)
78  typedef data_typet::const_iterator const_iterator;
79 
80  template <typename U>
81  const_iterator find(U &&u) const { return data.find(std::forward<U>(u)); }
82 
83  iterator begin() { return data.begin(); }
84  const_iterator begin() const { return data.begin(); }
85  const_iterator cbegin() const { return data.cbegin(); }
86 
87  iterator end() { return data.end(); }
88  const_iterator end() const { return data.end(); }
89  const_iterator cend() const { return data.cend(); }
90 
91  explicit entry_mapt(grapht< cfg_base_nodet<T, I> > &_container):
92  container(_container)
93  {
94  }
95 
97  {
98  auto e=data.insert(std::make_pair(t, 0));
99 
100  if(e.second)
101  e.first->second=container.add_node();
102 
103  return e.first->second;
104  }
105  };
106  entry_mapt entry_map;
107 
108 protected:
109  virtual void compute_edges_goto(
111  const goto_programt::instructiont &instruction,
113  entryt &entry);
114 
115  virtual void compute_edges_catch(
117  const goto_programt::instructiont &instruction,
119  entryt &entry);
120 
121  virtual void compute_edges_throw(
123  const goto_programt::instructiont &instruction,
125  entryt &entry);
126 
127  virtual void compute_edges_start_thread(
129  const goto_programt::instructiont &instruction,
131  entryt &entry);
132 
133  virtual void compute_edges_function_call(
134  const goto_functionst &goto_functions,
136  const goto_programt::instructiont &instruction,
138  entryt &entry);
139 
140  void compute_edges(
141  const goto_functionst &goto_functions,
143  I PC);
144 
145  void compute_edges(
146  const goto_functionst &goto_functions,
147  P &goto_program);
148 
149  void compute_edges(
150  const goto_functionst &goto_functions);
151 
152 public:
154  {
155  }
156 
157  virtual ~cfg_baset()
158  {
159  }
160 
162  const goto_functionst &goto_functions)
163  {
164  compute_edges(goto_functions);
165  }
166 
168  {
169  goto_functionst goto_functions;
170  compute_edges(goto_functions, goto_program);
171  }
172 
173  I get_first_node(P &program) const { return program.instructions.begin(); }
174  I get_last_node(P &program) const { return --program.instructions.end(); }
175  bool nodes_empty(P &program) const { return program.instructions.empty(); }
176 };
177 
178 template<class T,
179  typename P=const goto_programt,
180  typename I=goto_programt::const_targett>
181 class concurrent_cfg_baset:public virtual cfg_baset<T, P, I>
182 {
183 protected:
184  virtual void compute_edges_start_thread(
186  const goto_programt::instructiont &instruction,
188  typename cfg_baset<T, P, I>::entryt &entry);
189 };
190 
191 template<class T,
192  typename P=const goto_programt,
193  typename I=goto_programt::const_targett>
194 class procedure_local_cfg_baset:public virtual cfg_baset<T, P, I>
195 {
196 protected:
197  virtual void compute_edges_function_call(
198  const goto_functionst &goto_functions,
200  const goto_programt::instructiont &instruction,
202  typename cfg_baset<T, P, I>::entryt &entry);
203 };
204 
205 template<class T,
206  typename P=const goto_programt,
207  typename I=goto_programt::const_targett>
209  public concurrent_cfg_baset<T, P, I>,
210  public procedure_local_cfg_baset<T, P, I>
211 {
212 };
213 
214 template<class T, typename P, typename I>
217  const goto_programt::instructiont &instruction,
219  entryt &entry)
220 {
221  if(next_PC!=goto_program.instructions.end() &&
222  !instruction.guard.is_true())
223  this->add_edge(entry, entry_map[next_PC]);
224 
225  this->add_edge(entry, entry_map[instruction.get_target()]);
226 }
227 
228 template<class T, typename P, typename I>
231  const goto_programt::instructiont &instruction,
233  entryt &entry)
234 {
235  if(next_PC!=goto_program.instructions.end())
236  this->add_edge(entry, entry_map[next_PC]);
237 
238  // Not ideal, but preserves targets
239  // Ideally, the throw statements should have those as successors
240 
241  for(const auto &t : instruction.targets)
242  if(t!=goto_program.instructions.end())
243  this->add_edge(entry, entry_map[t]);
244 }
245 
246 template<class T, typename P, typename I>
249  const goto_programt::instructiont &instruction,
251  entryt &entry)
252 {
253  // no (trivial) successors
254 }
255 
256 template<class T, typename P, typename I>
259  const goto_programt::instructiont &instruction,
261  entryt &entry)
262 {
263  if(next_PC!=goto_program.instructions.end())
264  this->add_edge(entry, entry_map[next_PC]);
265 }
266 
267 template<class T, typename P, typename I>
270  const goto_programt::instructiont &instruction,
272  typename cfg_baset<T, P, I>::entryt &entry)
273 {
275  goto_program,
276  instruction,
277  next_PC,
278  entry);
279 
280  this->add_edge(entry, this->entry_map[instruction.get_target()]);
281 }
282 
283 template<class T, typename P, typename I>
285  const goto_functionst &goto_functions,
287  const goto_programt::instructiont &instruction,
289  entryt &entry)
290 {
291  const exprt &function=
292  to_code_function_call(instruction.code).function();
293 
294  if(function.id()!=ID_symbol)
295  return;
296 
297  const irep_idt &identifier=
298  to_symbol_expr(function).get_identifier();
299 
300  goto_functionst::function_mapt::const_iterator f_it=
301  goto_functions.function_map.find(identifier);
302 
303  if(f_it!=goto_functions.function_map.end() &&
304  f_it->second.body_available())
305  {
306  // get the first instruction
308  f_it->second.body.instructions.begin();
309 
311  f_it->second.body.instructions.end();
312 
313  goto_programt::const_targett last_it=e_it; last_it--;
314 
315  if(i_it!=e_it)
316  {
317  // nonempty function
318  this->add_edge(entry, entry_map[i_it]);
319 
320  // add the last instruction as predecessor of the return location
321  if(next_PC!=goto_program.instructions.end())
322  this->add_edge(entry_map[last_it], entry_map[next_PC]);
323  }
324  else if(next_PC!=goto_program.instructions.end())
325  {
326  // empty function
327  this->add_edge(entry, entry_map[next_PC]);
328  }
329  }
330  else if(next_PC!=goto_program.instructions.end())
331  this->add_edge(entry, entry_map[next_PC]);
332 }
333 
334 template<class T, typename P, typename I>
336  const goto_functionst &goto_functions,
338  const goto_programt::instructiont &instruction,
340  typename cfg_baset<T, P, I>::entryt &entry)
341 {
342  const exprt &function=
343  to_code_function_call(instruction.code).function();
344 
345  if(function.id()!=ID_symbol)
346  return;
347 
348  if(next_PC!=goto_program.instructions.end())
349  this->add_edge(entry, this->entry_map[next_PC]);
350 }
351 
352 template<class T, typename P, typename I>
354  const goto_functionst &goto_functions,
356  I PC)
357 {
358  const goto_programt::instructiont &instruction=*PC;
359  entryt entry=entry_map[PC];
360  (*this)[entry].PC=PC;
361  goto_programt::const_targett next_PC(PC);
362  next_PC++;
363 
364  // compute forward edges first
365  switch(instruction.type)
366  {
367  case GOTO:
368  compute_edges_goto(goto_program, instruction, next_PC, entry);
369  break;
370 
371  case CATCH:
372  compute_edges_catch(goto_program, instruction, next_PC, entry);
373  break;
374 
375  case THROW:
376  compute_edges_throw(goto_program, instruction, next_PC, entry);
377  break;
378 
379  case START_THREAD:
380  compute_edges_start_thread(
381  goto_program,
382  instruction,
383  next_PC,
384  entry);
385  break;
386 
387  case FUNCTION_CALL:
388  compute_edges_function_call(
389  goto_functions,
390  goto_program,
391  instruction,
392  next_PC,
393  entry);
394  break;
395 
396  case END_THREAD:
397  case END_FUNCTION:
398  // no successor
399  break;
400 
401  case ASSUME:
402  // false guard -> no successor
403  if(instruction.guard.is_false())
404  break;
405 
406  case ASSIGN:
407  case ASSERT:
408  case OTHER:
409  case RETURN:
410  case SKIP:
411  case LOCATION:
412  case ATOMIC_BEGIN:
413  case ATOMIC_END:
414  case DECL:
415  case DEAD:
416  if(next_PC!=goto_program.instructions.end())
417  this->add_edge(entry, entry_map[next_PC]);
418  break;
419 
420  case NO_INSTRUCTION_TYPE:
421  case INCOMPLETE_GOTO:
422  UNREACHABLE;
423  break;
424  }
425 }
426 
427 template<class T, typename P, typename I>
429  const goto_functionst &goto_functions,
430  P &goto_program)
431 {
432  for(I it=goto_program.instructions.begin();
433  it!=goto_program.instructions.end();
434  ++it)
435  compute_edges(goto_functions, goto_program, it);
436 }
437 
438 template<class T, typename P, typename I>
440  const goto_functionst &goto_functions)
441 {
442  forall_goto_functions(it, goto_functions)
443  if(it->second.body_available())
444  compute_edges(goto_functions, it->second.body);
445 }
446 
447 #endif // CPROVER_GOTO_PROGRAMS_CFG_H
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
I get_last_node(P &program) const
Definition: cfg.h:174
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
Definition: cfg.h:353
A generic directed graph with a parametric node type.
Definition: graph.h:133
data_typet::iterator iterator
Definition: cfg.h:76
iterator end()
Definition: cfg.h:87
entry_mapt entry_map
Definition: cfg.h:106
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
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:128
Goto Programs with Functions.
grapht< cfg_base_nodet< T, I > > & container
Definition: cfg.h:73
bool is_false() const
Definition: expr.cpp:131
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:215
bool is_true() const
Definition: expr.cpp:124
function_mapt function_map
bool nodes_empty(P &program) const
Definition: cfg.h:175
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:202
std::size_t entryt
Definition: cfg.h:65
const_iterator cbegin() const
Definition: cfg.h:85
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
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:229
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const_iterator find(U &&u) const
Definition: cfg.h:81
void operator()(const goto_functionst &goto_functions)
Definition: cfg.h:161
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
graph_nodet< empty_edget >::edgest edgest
Definition: cfg.h:29
void operator()(P &goto_program)
Definition: cfg.h:167
instructionst::const_iterator const_targett
Definition: goto_program.h:398
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:268
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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:335
data_typet::const_iterator const_iterator
Definition: cfg.h:78
entryt & operator[](const goto_programt::const_targett &t)
Definition: cfg.h:96
iterator begin()
Definition: cfg.h:83
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
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:247
A Template Class for Graphs.
node_indext add_node()
Definition: graph.h:146
graph_nodet< empty_edget >::edget edget
Definition: cfg.h:28
virtual ~cfg_baset()
Definition: cfg.h:157
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
cfg_baset()
Definition: cfg.h:153
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
Definition: cfg.h:91
#define UNREACHABLE
Definition: invariant.h:250
std::map< goto_programt::const_targett, entryt > data_typet
Definition: cfg.h:69
I get_first_node(P &program) const
Definition: cfg.h:173
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:284
goto_programt & goto_program
Definition: cover.cpp:63
data_typet data
Definition: cfg.h:70
#define forall_goto_functions(it, functions)
const_iterator end() const
Definition: cfg.h:88
This class represents a node in a directed graph.
Definition: graph.h:34
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:257
Definition: kdev_t.h:24
const_iterator cend() const
Definition: cfg.h:89
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
const_iterator begin() const
Definition: cfg.h:84