cprover
remove_skip.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "remove_skip.h"
13 
14 static bool is_skip(goto_programt::instructionst::iterator it)
15 {
16  // we won't remove labelled statements
17  // (think about error labels or the like)
18 
19  if(!it->labels.empty())
20  return false;
21 
22  if(it->is_skip())
23  return !it->code.get_bool(ID_explicit);
24 
25  if(it->is_goto())
26  {
27  if(it->guard.is_false())
28  return true;
29 
30  if(it->targets.size()!=1)
31  return false;
32 
33  goto_programt::instructionst::iterator next_it=it;
34  next_it++;
35 
36  // A branch to the next instruction is a skip
37  // We also require the guard to be 'true'
38  return it->guard.is_true() &&
39  it->targets.front()==next_it;
40  }
41 
42  if(it->is_other())
43  {
44  if(it->code.is_nil())
45  return true;
46 
47  const irep_idt &statement=it->code.get_statement();
48 
49  if(statement==ID_skip)
50  return true;
51  else if(statement==ID_expression)
52  {
53  const code_expressiont &code_expression=to_code_expression(it->code);
54  const exprt &expr=code_expression.expression();
55  if(expr.id()==ID_typecast &&
56  expr.type().id()==ID_empty &&
58  {
59  // something like (void)0
60  return true;
61  }
62  }
63 
64  return false;
65  }
66 
67  return false;
68 }
69 
71 void remove_skip(goto_programt &goto_program)
72 {
73  // This needs to be a fixed-point, as
74  // removing a skip can turn a goto into a skip.
75  std::size_t old_size;
76 
77  do
78  {
79  old_size=goto_program.instructions.size();
80 
81  // maps deleted instructions to their replacement
82  typedef std::map<goto_programt::targett, goto_programt::targett>
83  new_targetst;
84  new_targetst new_targets;
85 
86  // remove skip statements
87 
88  for(goto_programt::instructionst::iterator
89  it=goto_program.instructions.begin();
90  it!=goto_program.instructions.end();)
91  {
92  goto_programt::targett old_target=it;
93 
94  // for collecting labels
95  std::list<irep_idt> labels;
96 
97  while(is_skip(it))
98  {
99  // don't remove the last skip statement,
100  // it could be a target
101  if(it==--goto_program.instructions.end())
102  break;
103 
104  // save labels
105  labels.splice(labels.end(), it->labels);
106  it++;
107  }
108 
109  goto_programt::targett new_target=it;
110 
111  // save labels
112  it->labels.splice(it->labels.begin(), labels);
113 
114  if(new_target!=old_target)
115  {
116  for(; old_target!=new_target; ++old_target)
117  new_targets[old_target]=new_target; // remember the old targets
118  }
119  else
120  it++;
121  }
122 
123  // adjust gotos
124 
125  Forall_goto_program_instructions(i_it, goto_program)
126  if(i_it->is_goto() || i_it->is_start_thread() || i_it->is_catch())
127  {
128  for(goto_programt::instructiont::targetst::iterator
129  t_it=i_it->targets.begin();
130  t_it!=i_it->targets.end();
131  t_it++)
132  {
133  new_targetst::const_iterator
134  result=new_targets.find(*t_it);
135 
136  if(result!=new_targets.end())
137  *t_it=result->second;
138  }
139  }
140 
141  // now delete the skips -- we do so after adjusting the
142  // gotos to avoid dangling targets
143  for(const auto &new_target : new_targets)
144  goto_program.instructions.erase(new_target.first);
145 
146  // remove the last skip statement unless it's a target
147  goto_program.compute_incoming_edges();
148 
149  if(!goto_program.instructions.empty() &&
150  is_skip(--goto_program.instructions.end()) &&
151  !goto_program.instructions.back().is_target())
152  goto_program.instructions.pop_back();
153  }
154  while(goto_program.instructions.size()<old_size);
155 }
156 
158 void remove_skip(goto_functionst &goto_functions)
159 {
160  Forall_goto_functions(f_it, goto_functions)
161  remove_skip(f_it->second.body);
162 }
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
instructionst instructions
The list of instructions in the goto program.
typet & type()
Definition: expr.h:60
exprt & op()
Definition: std_expr.h:1739
An expression statement.
Definition: std_code.h:957
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:981
const irep_idt & id() const
Definition: irep.h:189
bool is_constant() const
Definition: expr.cpp:128
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
Base class for all expressions.
Definition: expr.h:46
#define Forall_goto_functions(it, functions)
const exprt & expression() const
Definition: std_code.h:970
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
static bool is_skip(goto_programt::instructionst::iterator it)
Definition: remove_skip.cpp:14
Program Transformation.