CBMC
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
24
27 const goto_programt::const_targett end, // exclusive
28 goto_programt &goto_program) // result
29{
30 PRECONDITION(start->location_number < end->location_number);
31 PRECONDITION(goto_program.empty());
32
33 // build map for branch targets inside the loop
34 typedef std::
35 map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
36 target_mapt;
37 target_mapt target_map;
38
39 unsigned i=0;
40
41 for(goto_programt::const_targett t=start; t!=end; t++, i++)
42 target_map[t]=i;
43
44 // make a copy
45 std::vector<goto_programt::targett> target_vector;
46 target_vector.reserve(target_map.size());
48
49 for(goto_programt::const_targett t=start; t!=end; t++)
50 {
51 // copy the instruction
53 goto_program.add(goto_programt::instructiont(*t));
54 unwind_log.insert(t_new, t->location_number);
55 target_vector.push_back(t_new); // store copied instruction
56 }
57
58 CHECK_RETURN(goto_program.instructions.size() == target_vector.size());
59
60 // adjust intra-segment gotos
61 for(std::size_t target_index = 0; target_index < target_vector.size();
63 {
65
66 if(!t->is_goto())
67 continue;
68
69 goto_programt::const_targett tgt=t->get_target();
70
71 target_mapt::const_iterator m_it=target_map.find(tgt);
72
73 if(m_it!=target_map.end())
74 {
75 unsigned j=m_it->second;
76
77 DATA_INVARIANT(j < target_vector.size(), "in bounds");
78 t->set_target(target_vector[j]);
79 }
80 }
81}
82
84 const irep_idt &function_id,
85 goto_programt &goto_program,
88 const unsigned k,
90{
91 std::vector<goto_programt::targett> iteration_points;
92 unwind(
93 function_id,
94 goto_program,
97 k,
100}
101
103 const irep_idt &function_id,
104 goto_programt &goto_program,
107 const unsigned k,
109 std::vector<goto_programt::targett> &iteration_points)
110{
112 PRECONDITION(loop_head->location_number < loop_exit->location_number);
113
114 // rest program after unwound part
116
118 {
120 rest_program.add(goto_programt::make_skip(loop_head->source_location()));
121
122 t->location_number=loop_head->location_number;
123
124 unwind_log.insert(t, loop_head->location_number);
125 }
127 {
129 }
130 else
131 {
136
138 t--;
139 DATA_INVARIANT(t->is_backwards_goto(), "must be backwards goto");
140
141 exprt exit_cond = false_exprt(); // default is false
142
143 if(!t->condition().is_true()) // cond in backedge
144 {
145 exit_cond = boolean_negate(t->condition());
146 }
147 else if(loop_head->is_goto())
148 {
149 if(loop_head->get_target()==loop_exit) // cond in forward edge
150 exit_cond = loop_head->condition();
151 }
152
153 if(
156 {
157 const std::string loop_number = std::to_string(t->loop_number);
159 source_location_annotated.set_property_class("unwind");
160 source_location_annotated.set_comment(
161 "unwinding assertion loop " + loop_number);
162 goto_programt::targett assertion = rest_program.add(
164 unwind_log.insert(assertion, loop_head->location_number);
165 }
166
167 if(
170 {
171 goto_programt::targett assumption =
173 exit_cond, loop_head->source_location()));
174 unwind_log.insert(assumption, loop_head->location_number);
175 }
176
177 }
178
179 CHECK_RETURN(!rest_program.empty());
180
181 // to be filled with copies of the loop body
183
184 if(k!=0)
185 {
186 iteration_points.resize(k);
187
188 // add a goto before the loop exit to guard against 'fall-out'
189
191 t_before--;
192
193 if(!t_before->is_goto() || !t_before->condition().is_true())
194 {
196 loop_exit,
198 goto_program.const_cast_target(loop_exit),
199 true_exprt(),
200 loop_exit->source_location()));
201 t_goto->location_number=loop_exit->location_number;
202
203 unwind_log.insert(t_goto, loop_exit->location_number);
204 }
205
206 // add a skip before the loop exit
207
209 loop_exit, goto_programt::make_skip(loop_head->source_location()));
210 t_skip->location_number=loop_head->location_number;
211
212 unwind_log.insert(t_skip, loop_exit->location_number);
213
214 // where to go for the next iteration
216
217 // record the exit point of first iteration
219
220 // re-direct any branches that go to loop_head to loop_iter
221
223 t=goto_program.const_cast_target(loop_head);
224 t!=loop_iter; t++)
225 {
226 if(!t->is_goto())
227 continue;
228
229 if(t->get_target()==loop_head)
230 t->set_target(loop_iter);
231 }
232
233 // k-1 additional copies
234 for(unsigned i=1; i<k; i++)
235 {
238 CHECK_RETURN(!tmp_program.instructions.empty());
239
240 iteration_points[i]=--tmp_program.instructions.end();
241
242 copies.destructive_append(tmp_program);
243 }
244 }
245 else
246 {
247 // insert skip for loop body
248
250 loop_head, goto_programt::make_skip(loop_head->source_location()));
251 t_skip->location_number=loop_head->location_number;
252
253 unwind_log.insert(t_skip, loop_head->location_number);
254
255 // redirect gotos into loop body
256 for(auto &instruction : goto_program.instructions)
257 {
258 if(!instruction.is_goto())
259 continue;
260
261 goto_programt::const_targett t = instruction.get_target();
262
263 if(t->location_number>=loop_head->location_number &&
264 t->location_number<loop_exit->location_number)
265 {
266 instruction.set_target(t_skip);
267 }
268 }
269
270 // delete loop body
271 goto_program.instructions.erase(loop_head, loop_exit);
272 }
273
274 // after unwound part
275 copies.destructive_append(rest_program);
276
277 // now insert copies before loop_exit
278 goto_program.destructive_insert(loop_exit, copies);
279}
280
282 const irep_idt &function_id,
283 goto_programt &goto_program,
284 const unwindsett &unwindset,
286{
287 for(goto_programt::const_targett i_it=goto_program.instructions.begin();
288 i_it!=goto_program.instructions.end();)
289 {
290#ifdef DEBUG
291 std::cout << "Instruction:\n";
292 i_it->output(std::cout);
293#endif
294
295 if(!i_it->is_backwards_goto())
296 {
297 i_it++;
298 continue;
299 }
300
301 PRECONDITION(!function_id.empty());
302 const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it);
303
304 auto limit=unwindset.get_limit(loop_id, 0);
305
306 if(!limit.has_value())
307 {
308 // no unwinding given
309 i_it++;
310 continue;
311 }
312
315 loop_exit++;
316 CHECK_RETURN(loop_exit != goto_program.instructions.end());
317
318 unwind(
319 function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
320
321 // necessary as we change the goto program in the previous line
323 }
324}
325
327 goto_functionst &goto_functions,
328 const unwindsett &unwindset,
330{
331 for(auto &gf_entry : goto_functions.function_map)
332 {
333 goto_functionst::goto_functiont &goto_function = gf_entry.second;
334
335 if(!goto_function.body_available())
336 continue;
337
338#ifdef DEBUG
339 std::cout << "Function: " << gf_entry.first << '\n';
340#endif
341
342 goto_programt &goto_program=goto_function.body;
343
344 unwind(gf_entry.first, goto_program, unwindset, unwind_strategy);
345 }
346}
347
348// call after calling goto_functions.update()!
350{
352 json_arrayt &json_unwound=json_result["unwound"].make_array();
353
354 for(location_mapt::const_iterator it=location_map.begin();
355 it!=location_map.end(); it++)
356 {
357 goto_programt::const_targett target=it->first;
358 unsigned location_number=it->second;
359
360 json_objectt object{
361 {"originalLocationNumber", json_numbert(std::to_string(location_number))},
362 {"newLocationNumber",
363 json_numbert(std::to_string(target->location_number))}};
364
365 json_unwound.push_back(std::move(object));
366 }
367
368 return std::move(json_result);
369}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3200
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
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:326
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition unwind.cpp:25
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:83
unwind_logt unwind_log
Definition unwind.h:115
Definition json.h:27
The Boolean constant true.
Definition std_expr.h:3191
std::optional< 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
Definition expr_util.cpp:98
Deprecated expression utility functions.
Goto Programs with Functions.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
jsont output_log_json() const
Definition unwind.cpp:349
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition unwind.h:99
location_mapt location_map
Definition unwind.h:112
Loop unwinding.
Loop unwinding.