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