cprover
Loading...
Searching...
No Matches
unwind.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop unwinding
4
5Author: Daniel Kroening, kroening@kroening.com
6 Daniel Poetzl
7
8\*******************************************************************/
9
12
13#include "unwind.h"
14
15#ifdef DEBUG
16#include <iostream>
17#endif
18
19#include <util/expr_util.h>
20#include <util/std_expr.h>
21
23
24#include "unwindset.h"
25
28 const goto_programt::const_targett end, // exclusive
29 goto_programt &goto_program) // result
30{
31 assert(start->location_number<end->location_number);
32 assert(goto_program.empty());
33
34 // build map for branch targets inside the loop
35 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
36 target_mapt target_map;
37
38 unsigned i=0;
39
40 for(goto_programt::const_targett t=start; t!=end; t++, i++)
41 target_map[t]=i;
42
43 // make a copy
44 std::vector<goto_programt::targett> target_vector;
45 target_vector.reserve(target_map.size());
46 assert(target_vector.empty());
47
48 for(goto_programt::const_targett t=start; t!=end; t++)
49 {
50 // copy the instruction
52 goto_program.add(goto_programt::instructiont(*t));
53 unwind_log.insert(t_new, t->location_number);
54 target_vector.push_back(t_new); // store copied instruction
55 }
56
57 assert(goto_program.instructions.size()==target_vector.size());
58
59 // adjust intra-segment gotos
60 for(std::size_t target_index = 0; target_index < target_vector.size();
61 target_index++)
62 {
63 goto_programt::targett t = target_vector[target_index];
64
65 if(!t->is_goto())
66 continue;
67
68 goto_programt::const_targett tgt=t->get_target();
69
70 target_mapt::const_iterator m_it=target_map.find(tgt);
71
72 if(m_it!=target_map.end())
73 {
74 unsigned j=m_it->second;
75
76 assert(j<target_vector.size());
77 t->set_target(target_vector[j]);
78 }
79 }
80}
81
83 const irep_idt &function_id,
84 goto_programt &goto_program,
85 const goto_programt::const_targett loop_head,
86 const goto_programt::const_targett loop_exit,
87 const unsigned k,
88 const unwind_strategyt unwind_strategy)
89{
90 std::vector<goto_programt::targett> iteration_points;
91 unwind(
92 function_id,
93 goto_program,
94 loop_head,
95 loop_exit,
96 k,
97 unwind_strategy,
98 iteration_points);
99}
100
102 const irep_idt &function_id,
103 goto_programt &goto_program,
104 const goto_programt::const_targett loop_head,
105 const goto_programt::const_targett loop_exit,
106 const unsigned k,
107 const unwind_strategyt unwind_strategy,
108 std::vector<goto_programt::targett> &iteration_points)
109{
110 assert(iteration_points.empty());
111 assert(loop_head->location_number<loop_exit->location_number);
112
113 // rest program after unwound part
114 goto_programt rest_program;
115
116 if(unwind_strategy==unwind_strategyt::PARTIAL)
117 {
119 rest_program.add(goto_programt::make_skip(loop_head->source_location()));
120
121 t->location_number=loop_head->location_number;
122
123 unwind_log.insert(t, loop_head->location_number);
124 }
125 else if(unwind_strategy==unwind_strategyt::CONTINUE)
126 {
127 copy_segment(loop_head, loop_exit, rest_program);
128 }
129 else
130 {
132 t--;
133 assert(t->is_backwards_goto());
134
135 exprt exit_cond = false_exprt(); // default is false
136
137 if(!t->get_condition().is_true()) // cond in backedge
138 {
139 exit_cond = boolean_negate(t->get_condition());
140 }
141 else if(loop_head->is_goto())
142 {
143 if(loop_head->get_target()==loop_exit) // cond in forward edge
144 exit_cond = loop_head->get_condition();
145 }
146
148
149 if(unwind_strategy==unwind_strategyt::ASSERT)
150 {
151 new_t = rest_program.add(goto_programt::make_assertion(exit_cond));
152 }
153 else if(unwind_strategy==unwind_strategyt::ASSUME)
154 {
155 new_t = rest_program.add(goto_programt::make_assumption(exit_cond));
156 }
157 else
159
160 new_t->source_location_nonconst() = loop_head->source_location();
161 new_t->location_number=loop_head->location_number;
162 unwind_log.insert(new_t, loop_head->location_number);
163 }
164
165 assert(!rest_program.empty());
166
167 // to be filled with copies of the loop body
168 goto_programt copies;
169
170 if(k!=0)
171 {
172 iteration_points.resize(k);
173
174 // add a goto before the loop exit to guard against 'fall-out'
175
176 goto_programt::const_targett t_before=loop_exit;
177 t_before--;
178
179 if(!t_before->is_goto() || !t_before->get_condition().is_true())
180 {
181 goto_programt::targett t_goto = goto_program.insert_before(
182 loop_exit,
184 goto_program.const_cast_target(loop_exit),
185 true_exprt(),
186 loop_exit->source_location()));
187 t_goto->location_number=loop_exit->location_number;
188
189 unwind_log.insert(t_goto, loop_exit->location_number);
190 }
191
192 // add a skip before the loop exit
193
194 goto_programt::targett t_skip = goto_program.insert_before(
195 loop_exit, goto_programt::make_skip(loop_head->source_location()));
196 t_skip->location_number=loop_head->location_number;
197
198 unwind_log.insert(t_skip, loop_exit->location_number);
199
200 // where to go for the next iteration
201 goto_programt::targett loop_iter=t_skip;
202
203 // record the exit point of first iteration
204 iteration_points[0]=loop_iter;
205
206 // re-direct any branches that go to loop_head to loop_iter
207
209 t=goto_program.const_cast_target(loop_head);
210 t!=loop_iter; t++)
211 {
212 if(!t->is_goto())
213 continue;
214
215 if(t->get_target()==loop_head)
216 t->set_target(loop_iter);
217 }
218
219 // k-1 additional copies
220 for(unsigned i=1; i<k; i++)
221 {
222 goto_programt tmp_program;
223 copy_segment(loop_head, loop_exit, tmp_program);
224 assert(!tmp_program.instructions.empty());
225
226 iteration_points[i]=--tmp_program.instructions.end();
227
228 copies.destructive_append(tmp_program);
229 }
230 }
231 else
232 {
233 // insert skip for loop body
234
235 goto_programt::targett t_skip = goto_program.insert_before(
236 loop_head, goto_programt::make_skip(loop_head->source_location()));
237 t_skip->location_number=loop_head->location_number;
238
239 unwind_log.insert(t_skip, loop_head->location_number);
240
241 // redirect gotos into loop body
242 for(auto &instruction : goto_program.instructions)
243 {
244 if(!instruction.is_goto())
245 continue;
246
247 goto_programt::const_targett t = instruction.get_target();
248
249 if(t->location_number>=loop_head->location_number &&
250 t->location_number<loop_exit->location_number)
251 {
252 instruction.set_target(t_skip);
253 }
254 }
255
256 // delete loop body
257 goto_program.instructions.erase(loop_head, loop_exit);
258 }
259
260 // after unwound part
261 copies.destructive_append(rest_program);
262
263 // now insert copies before loop_exit
264 goto_program.destructive_insert(loop_exit, copies);
265}
266
268 const irep_idt &function_id,
269 goto_programt &goto_program,
270 const unwindsett &unwindset,
271 const unwind_strategyt unwind_strategy)
272{
273 for(goto_programt::const_targett i_it=goto_program.instructions.begin();
274 i_it!=goto_program.instructions.end();)
275 {
276#ifdef DEBUG
277 symbol_tablet st;
278 namespacet ns(st);
279 std::cout << "Instruction:\n";
280 goto_program.output_instruction(ns, function_id, std::cout, *i_it);
281#endif
282
283 if(!i_it->is_backwards_goto())
284 {
285 i_it++;
286 continue;
287 }
288
289 PRECONDITION(!function_id.empty());
290 const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it);
291
292 auto limit=unwindset.get_limit(loop_id, 0);
293
294 if(!limit.has_value())
295 {
296 // no unwinding given
297 i_it++;
298 continue;
299 }
300
301 goto_programt::const_targett loop_head=i_it->get_target();
302 goto_programt::const_targett loop_exit=i_it;
303 loop_exit++;
304 assert(loop_exit!=goto_program.instructions.end());
305
306 unwind(
307 function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
308
309 // necessary as we change the goto program in the previous line
310 i_it=loop_exit;
311 }
312}
313
315 goto_functionst &goto_functions,
316 const unwindsett &unwindset,
317 const unwind_strategyt unwind_strategy)
318{
319 for(auto &gf_entry : goto_functions.function_map)
320 {
321 goto_functionst::goto_functiont &goto_function = gf_entry.second;
322
323 if(!goto_function.body_available())
324 continue;
325
326#ifdef DEBUG
327 std::cout << "Function: " << gf_entry.first << '\n';
328#endif
329
330 goto_programt &goto_program=goto_function.body;
331
332 unwind(gf_entry.first, goto_program, unwindset, unwind_strategy);
333 }
334}
335
336// call after calling goto_functions.update()!
338{
339 json_objectt json_result;
340 json_arrayt &json_unwound=json_result["unwound"].make_array();
341
342 for(location_mapt::const_iterator it=location_map.begin();
343 it!=location_map.end(); it++)
344 {
345 goto_programt::const_targett target=it->first;
346 unsigned location_number=it->second;
347
348 json_objectt object{
349 {"originalLocationNumber", json_numbert(std::to_string(location_number))},
350 {"newLocationNumber",
351 json_numbert(std::to_string(target->location_number))}};
352
353 json_unwound.push_back(std::move(object));
354 }
355
356 return std::move(json_result);
357}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Base class for all expressions.
Definition expr.h:54
const source_locationt & source_location() const
Definition expr.h:230
The Boolean constant false.
Definition std_expr.h:2865
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition unwind.cpp:314
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition unwind.cpp:26
void unwind(const irep_idt &function_id, goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
Definition unwind.cpp:82
unwind_logt unwind_log
Definition unwind.h:104
jsont & push_back(const jsont &json)
Definition json.h:212
Definition json.h:27
json_arrayt & make_array()
Definition json.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table.
The Boolean constant true.
Definition std_expr.h:2856
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Goto Programs with Functions.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
jsont output_log_json() const
Definition unwind.cpp:337
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition unwind.h:92
location_mapt location_map
Definition unwind.h:101
Loop unwinding.
Loop unwinding.