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->guard.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->guard.is_true() &&
50  it->get_target()==next_it;
51  }
52 
53  if(it->is_other())
54  {
55  if(it->code.is_nil())
56  return true;
57 
58  const irep_idt &statement=it->code.get_statement();
59 
60  if(statement==ID_skip)
61  return true;
62  else if(statement==ID_expression)
63  {
64  const code_expressiont &code_expression=to_code_expression(it->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  Forall_goto_functions(f_it, goto_functions)
198  remove_skip(
199  f_it->second.body,
200  f_it->second.body.instructions.begin(),
201  f_it->second.body.instructions.end());
202 
203  // we may remove targets
204  goto_functions.update();
205 }
206 
207 void remove_skip(goto_modelt &goto_model)
208 {
209  remove_skip(goto_model.goto_functions);
210 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1539
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:506
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:537
symbol_table_baset::end
virtual iteratort end()=0
irept::id
const irep_idt & id() const
Definition: irep.h:259
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
symbol_table_baset::begin
virtual iteratort begin()=0
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
goto_functionst::update
void update()
Definition: goto_functions.h:91
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1518
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
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1504