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->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=to_code_expression(it->code);
64  const exprt &expr=code_expression.expression();
65  if(expr.id()==ID_typecast &&
66  expr.type().id()==ID_empty &&
67  to_typecast_expr(expr).op().is_constant())
68  {
69  // something like (void)0
70  return true;
71  }
72  }
73 
74  return false;
75  }
76 
77  return false;
78 }
79 
86  goto_programt &goto_program,
89 {
90  // This needs to be a fixed-point, as
91  // removing a skip can turn a goto into a skip.
92  std::size_t old_size;
93 
94  do
95  {
96  old_size=goto_program.instructions.size();
97 
98  // maps deleted instructions to their replacement
99  typedef std::map<goto_programt::targett, goto_programt::targett>
100  new_targetst;
101  new_targetst new_targets;
102 
103  // remove skip statements
104 
105  for(goto_programt::instructionst::iterator it = begin; it != end;)
106  {
107  goto_programt::targett old_target=it;
108 
109  // for collecting labels
110  std::list<irep_idt> labels;
111 
112  while(is_skip(goto_program, it, true))
113  {
114  // don't remove the last skip statement,
115  // it could be a target
116  if(
117  it == std::prev(end) ||
118  (std::next(it)->is_end_function() &&
119  (!labels.empty() || !it->labels.empty())))
120  {
121  break;
122  }
123 
124  // save labels
125  labels.splice(labels.end(), it->labels);
126  it++;
127  }
128 
129  goto_programt::targett new_target=it;
130 
131  // save labels
132  it->labels.splice(it->labels.begin(), labels);
133 
134  if(new_target!=old_target)
135  {
136  for(; old_target!=new_target; ++old_target)
137  new_targets[old_target]=new_target; // remember the old targets
138  }
139  else
140  it++;
141  }
142 
143  // adjust gotos across the full goto program body
144  for(auto &ins : goto_program.instructions)
145  {
146  if(ins.is_goto() || ins.is_start_thread() || ins.is_catch())
147  {
148  for(auto &target : ins.targets)
149  {
150  new_targetst::const_iterator result = new_targets.find(target);
151 
152  if(result!=new_targets.end())
153  target = result->second;
154  }
155  }
156  }
157 
158  while(new_targets.find(begin) != new_targets.end())
159  ++begin;
160 
161  // now delete the skips -- we do so after adjusting the
162  // gotos to avoid dangling targets
163  for(const auto &new_target : new_targets)
164  goto_program.instructions.erase(new_target.first);
165 
166  // remove the last skip statement unless it's a target
167  goto_program.compute_target_numbers();
168 
169  if(begin != end)
170  {
171  goto_programt::targett last = std::prev(end);
172  if(begin == last)
173  ++begin;
174 
175  if(is_skip(goto_program, last) && !last->is_target())
176  goto_program.instructions.erase(last);
177  }
178  }
179  while(goto_program.instructions.size()<old_size);
180 }
181 
183 void remove_skip(goto_programt &goto_program)
184 {
185  remove_skip(
186  goto_program,
187  goto_program.instructions.begin(),
188  goto_program.instructions.end());
189 
190  goto_program.update();
191 }
192 
194 void remove_skip(goto_functionst &goto_functions)
195 {
196  Forall_goto_functions(f_it, goto_functions)
197  remove_skip(
198  f_it->second.body,
199  f_it->second.body.instructions.begin(),
200  f_it->second.body.instructions.end());
201 
202  // we may remove targets
203  goto_functions.update();
204 }
205 
206 void remove_skip(goto_modelt &goto_model)
207 {
208  remove_skip(goto_model.goto_functions);
209 }
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:1844
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:85
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:572
irept::id
const irep_idt & id() const
Definition: irep.h:418
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:2047
goto_functionst::update
void update()
Definition: goto_functions.h:81
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1817
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:30
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810