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(
110  const goto_programt &goto_program,
111  const goto_programt::instructiont &instruction,
113  entryt &entry);
114 
115  virtual void compute_edges_catch(
116  const goto_programt &goto_program,
117  const goto_programt::instructiont &instruction,
119  entryt &entry);
120 
121  virtual void compute_edges_throw(
122  const goto_programt &goto_program,
123  const goto_programt::instructiont &instruction,
125  entryt &entry);
126 
127  virtual void compute_edges_start_thread(
128  const goto_programt &goto_program,
129  const goto_programt::instructiont &instruction,
131  entryt &entry);
132 
133  virtual void compute_edges_function_call(
134  const goto_functionst &goto_functions,
135  const goto_programt &goto_program,
136  const goto_programt::instructiont &instruction,
138  entryt &entry);
139 
140  void compute_edges(
141  const goto_functionst &goto_functions,
142  const goto_programt &goto_program,
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 
167  void operator()(P &goto_program)
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(
185  const goto_programt &goto_program,
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,
199  const goto_programt &goto_program,
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>
216  const goto_programt &goto_program,
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>
230  const goto_programt &goto_program,
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>
248  const goto_programt &,
251  entryt &)
252 {
253  // no (trivial) successors
254 }
255 
256 template<class T, typename P, typename I>
258  const goto_programt &goto_program,
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>
269  const goto_programt &goto_program,
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,
286  const goto_programt &goto_program,
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 &,
337  const goto_programt &goto_program,
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,
355  const goto_programt &goto_program,
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
cfg_baset::entry_mapt::find
const_iterator find(U &&u) const
Definition: cfg.h:81
cfg_baset::~cfg_baset
virtual ~cfg_baset()
Definition: cfg.h:157
procedure_local_cfg_baset::compute_edges_function_call
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
cfg_baset::operator()
void operator()(P &goto_program)
Definition: cfg.h:167
cfg_base_nodet::PC
I PC
Definition: cfg.h:31
data
Definition: kdev_t.h:24
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
concurrent_cfg_baset
Definition: cfg.h:181
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:167
grapht::add_node
node_indext add_node()
Definition: graph.h:180
cfg_baset::entry_mapt::container
grapht< cfg_base_nodet< T, I > > & container
Definition: cfg.h:73
exprt
Base class for all expressions.
Definition: expr.h:54
cfg_baset::entry_mapt::operator[]
entryt & operator[](const goto_programt::const_targett &t)
Definition: cfg.h:96
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
empty_cfg_nodet
Definition: cfg.h:20
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
cfg_baset::compute_edges_throw
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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
cfg_baset::compute_edges_start_thread
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
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
cfg_baset::entry_mapt::data
data_typet data
Definition: cfg.h:70
procedure_local_concurrent_cfg_baset
Definition: cfg.h:208
cfg_baset::cfg_baset
cfg_baset()
Definition: cfg.h:153
THROW
Definition: goto_program.h:50
GOTO
Definition: goto_program.h:34
cfg_baset::entry_mapt
Definition: cfg.h:67
cfg_baset::get_first_node
I get_first_node(P &program) const
Definition: cfg.h:173
cfg_base_nodet::edgest
graph_nodet< empty_edget >::edgest edgest
Definition: cfg.h:29
cfg_baset::compute_edges_function_call
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::instructiont::code
codet code
Definition: goto_program.h:181
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
cfg_baset::get_last_node
I get_last_node(P &program) const
Definition: cfg.h:174
NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
OTHER
Definition: goto_program.h:37
cfg_baset::compute_edges
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
Definition: cfg.h:353
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
cfg_baset::entry_mapt::end
const_iterator end() const
Definition: cfg.h:88
END_FUNCTION
Definition: goto_program.h:42
SKIP
Definition: goto_program.h:38
cfg_baset::entry_mapt::entry_mapt
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
Definition: cfg.h:91
cfg_baset::entry_mapt::cbegin
const_iterator cbegin() const
Definition: cfg.h:85
RETURN
Definition: goto_program.h:45
cfg_baset::entry_map
entry_mapt entry_map
Definition: cfg.h:106
cfg_baset
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
Definition: cfg.h:62
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
ASSIGN
Definition: goto_program.h:46
cfg_baset::nodes_empty
bool nodes_empty(P &program) const
Definition: cfg.h:175
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
cfg_baset::entry_mapt::const_iterator
data_typet::const_iterator const_iterator
Definition: cfg.h:78
CATCH
Definition: goto_program.h:51
graph.h
DECL
Definition: goto_program.h:47
cfg_baset::entry_mapt::data_typet
std::map< goto_programt::const_targett, entryt > data_typet
Definition: cfg.h:69
graph_nodet
This class represents a node in a directed graph.
Definition: graph.h:35
cfg_baset::compute_edges_goto
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
ASSUME
Definition: goto_program.h:35
procedure_local_cfg_baset
Definition: cfg.h:194
cfg_base_nodet::edget
graph_nodet< empty_edget >::edget edget
Definition: cfg.h:28
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
Definition: goto_program.h:49
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
cfg_baset::entryt
std::size_t entryt
Definition: cfg.h:65
cfg_base_nodet
Definition: cfg.h:26
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
DEAD
Definition: goto_program.h:48
cfg_baset::compute_edges_catch
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
cfg_baset::entry_mapt::begin
iterator begin()
Definition: cfg.h:83
cfg_baset::operator()
void operator()(const goto_functionst &goto_functions)
Definition: cfg.h:161
ATOMIC_BEGIN
Definition: goto_program.h:43
LOCATION
Definition: goto_program.h:41
ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
cfg_baset::entry_mapt::cend
const_iterator cend() const
Definition: cfg.h:89
cfg_baset::entry_mapt::begin
const_iterator begin() const
Definition: cfg.h:84
concurrent_cfg_baset::compute_edges_start_thread
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
cfg_baset::entry_mapt::iterator
data_typet::iterator iterator
Definition: cfg.h:76
goto_programt::instructiont::get_target
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
Definition: goto_program.h:52
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
cfg_baset::entry_mapt::end
iterator end()
Definition: cfg.h:87