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 #include "goto_model.h"
14 
15 #include <util/std_code.h>
16 
27 bool is_skip(
28  const goto_programt &body,
30  bool ignore_labels)
31 {
32  if(!ignore_labels && !it->labels.empty())
33  return false;
34 
35  if(it->is_skip())
36  return !it->get_code().get_bool(ID_explicit);
37 
38  if(it->is_goto())
39  {
40  if(it->get_condition().is_false())
41  return true;
42 
43  goto_programt::const_targett next_it = it;
44  next_it++;
45 
46  if(next_it == body.instructions.end())
47  return false;
48 
49  // A branch to the next instruction is a skip
50  // We also require the guard to be 'true'
51  return it->get_condition().is_true() && it->get_target() == next_it;
52  }
53 
54  if(it->is_other())
55  {
56  if(it->get_other().is_nil())
57  return true;
58 
59  const irep_idt &statement = it->get_other().get_statement();
60 
61  if(statement==ID_skip)
62  return true;
63  else if(statement==ID_expression)
64  {
65  const code_expressiont &code_expression =
66  to_code_expression(it->get_code());
67  const exprt &expr=code_expression.expression();
68  if(expr.id()==ID_typecast &&
69  expr.type().id()==ID_empty &&
70  to_typecast_expr(expr).op().is_constant())
71  {
72  // something like (void)0
73  return true;
74  }
75  }
76 
77  return false;
78  }
79 
80  return false;
81 }
82 
89  goto_programt &goto_program,
92 {
93  // This needs to be a fixed-point, as
94  // removing a skip can turn a goto into a skip.
95  std::size_t old_size;
96 
97  do
98  {
99  old_size=goto_program.instructions.size();
100 
101  // maps deleted instructions to their replacement
102  typedef std::map<goto_programt::targett, goto_programt::targett>
103  new_targetst;
104  new_targetst new_targets;
105 
106  // remove skip statements
107 
108  for(goto_programt::instructionst::iterator it = begin; it != end;)
109  {
110  goto_programt::targett old_target=it;
111 
112  // for collecting labels
113  std::list<irep_idt> labels;
114 
115  while(is_skip(goto_program, it, true))
116  {
117  // don't remove the last skip statement,
118  // it could be a target
119  if(
120  it == std::prev(end) ||
121  (std::next(it)->is_end_function() &&
122  (!labels.empty() || !it->labels.empty())))
123  {
124  break;
125  }
126 
127  // save labels
128  labels.splice(labels.end(), it->labels);
129  it++;
130  }
131 
132  goto_programt::targett new_target=it;
133 
134  // save labels
135  it->labels.splice(it->labels.begin(), labels);
136 
137  if(new_target!=old_target)
138  {
139  for(; old_target!=new_target; ++old_target)
140  new_targets[old_target]=new_target; // remember the old targets
141  }
142  else
143  it++;
144  }
145 
146  // adjust gotos across the full goto program body
147  for(auto &ins : goto_program.instructions)
148  {
149  if(ins.is_goto() || ins.is_start_thread() || ins.is_catch())
150  {
151  for(auto &target : ins.targets)
152  {
153  new_targetst::const_iterator result = new_targets.find(target);
154 
155  if(result!=new_targets.end())
156  target = result->second;
157  }
158  }
159  }
160 
161  while(new_targets.find(begin) != new_targets.end())
162  ++begin;
163 
164  // now delete the skips -- we do so after adjusting the
165  // gotos to avoid dangling targets
166  for(const auto &new_target : new_targets)
167  goto_program.instructions.erase(new_target.first);
168 
169  // remove the last skip statement unless it's a target
170  goto_program.compute_target_numbers();
171 
172  if(begin != end)
173  {
174  goto_programt::targett last = std::prev(end);
175  if(begin == last)
176  ++begin;
177 
178  if(is_skip(goto_program, last) && !last->is_target())
179  goto_program.instructions.erase(last);
180  }
181  }
182  while(goto_program.instructions.size()<old_size);
183 }
184 
186 void remove_skip(goto_programt &goto_program)
187 {
188  remove_skip(
189  goto_program,
190  goto_program.instructions.begin(),
191  goto_program.instructions.end());
192 
193  goto_program.update();
194 }
195 
197 void remove_skip(goto_functionst &goto_functions)
198 {
199  for(auto &gf_entry : goto_functions.function_map)
200  {
201  remove_skip(
202  gf_entry.second.body,
203  gf_entry.second.body.instructions.begin(),
204  gf_entry.second.body.instructions.end());
205  }
206 
207  // we may remove targets
208  goto_functions.update();
209 }
210 
211 void remove_skip(goto_modelt &goto_model)
212 {
213  remove_skip(goto_model.goto_functions);
214 }
codet representation of an expression statement.
Definition: std_code.h:1394
const exprt & expression() const
Definition: std_code.h:1401
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
void compute_target_numbers()
Compute the target numbers.
const irep_idt & id() const
Definition: irep.h:396
Symbol Table + CFG.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
bool is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
Definition: remove_skip.cpp:27
Program Transformation.
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29