cprover
basic_blocks.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Group Basic Blocks in Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "basic_blocks.h"
13 
15 void basic_blocks(goto_programt &goto_program,
16  unsigned max_block_size)
17 {
18  // get the targets
19  typedef std::set<goto_programt::const_targett> targetst;
20 
21  targetst targets;
22 
23  for(goto_programt::instructionst::iterator
24  i_it=goto_program.instructions.begin();
25  i_it!=goto_program.instructions.end();
26  i_it++)
27  if(i_it->is_goto())
28  for(const auto &target : i_it->targets)
29  targets.insert(target);
30 
31  // Scan program
32  for(goto_programt::instructionst::iterator
33  it=goto_program.instructions.begin();
34  it!=goto_program.instructions.end();
35  ) // intentionally no it++
36  {
37  // gotos and empty code are left unchanged
38  if(it->is_goto() || it->is_dead() ||
39  it->is_assert() || it->is_assume() ||
40  it->is_atomic_begin() || it->is_atomic_end() ||
41  it->is_end_thread() || it->is_start_thread() ||
42  it->is_end_function() || it->is_location() ||
43  it->is_skip() || it->is_function_call() ||
44  it->is_decl())
45  it++;
46  else if(it->is_other() || it->is_assign())
47  {
48  if(it->code.is_nil())
49  it++;
50  else
51  {
52  unsigned count=0;
53 
54  // this is the start of a new block
55  targetst::iterator t_it; // iterator for searching targets
56 
57  // find the end of the block
58  goto_programt::instructionst::iterator end_block = it;
59  do
60  {
61  end_block++;
62  count++;
63  if(end_block!=goto_program.instructions.end())
64  t_it=targets.find(end_block);
65 
66  if(max_block_size!=0 && count>=max_block_size)
67  break;
68  }
69  while(end_block!=goto_program.instructions.end() &&
70  (end_block->is_other() || end_block->is_assign()) &&
71  t_it==targets.end());
72 
73  // replace it with the code of the block
74 
75  {
76  code_blockt new_block;
77 
78  for(goto_programt::instructionst::iterator stmt = it;
79  stmt != end_block;
80  stmt++)
81  if(!stmt->code.is_nil())
82  new_block.move_to_operands(stmt->code);
83 
84  it->code.swap(new_block);
85  it++;
86  if(it!=goto_program.instructions.end())
87  it=goto_program.instructions.erase(it, end_block);
88  }
89  }
90  }
91  else
92  assert(false);
93  }
94 }
instructionst instructions
The list of instructions in the goto program.
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
Group Basic Blocks in Goto Program.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void basic_blocks(goto_programt &goto_program, unsigned max_block_size)
convert basic blocks into single expressions of type "block"
Sequential composition.
Definition: std_code.h:63