cprover
Loading...
Searching...
No Matches
remove_skip.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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
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
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
186void remove_skip(goto_programt &goto_program)
187{
189 goto_program,
190 goto_program.instructions.begin(),
191 goto_program.instructions.end());
192
193 goto_program.update();
194}
195
197void remove_skip(goto_functionst &goto_functions)
198{
199 for(auto &gf_entry : goto_functions.function_map)
200 {
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
211void 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.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
instructionst::iterator targett
instructionst::const_iterator const_targett
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
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).
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