CBMC
unwind.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop unwinding
4 
5 Author: 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 
27  const goto_programt::const_targett start,
28  const goto_programt::const_targett end, // exclusive
29  goto_programt &goto_program) // result
30 {
31  PRECONDITION(start->location_number < end->location_number);
32  PRECONDITION(goto_program.empty());
33 
34  // build map for branch targets inside the loop
35  typedef std::
36  map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
37  target_mapt;
38  target_mapt target_map;
39 
40  unsigned i=0;
41 
42  for(goto_programt::const_targett t=start; t!=end; t++, i++)
43  target_map[t]=i;
44 
45  // make a copy
46  std::vector<goto_programt::targett> target_vector;
47  target_vector.reserve(target_map.size());
48  CHECK_RETURN(target_vector.empty());
49 
50  for(goto_programt::const_targett t=start; t!=end; t++)
51  {
52  // copy the instruction
54  goto_program.add(goto_programt::instructiont(*t));
55  unwind_log.insert(t_new, t->location_number);
56  target_vector.push_back(t_new); // store copied instruction
57  }
58 
59  CHECK_RETURN(goto_program.instructions.size() == target_vector.size());
60 
61  // adjust intra-segment gotos
62  for(std::size_t target_index = 0; target_index < target_vector.size();
63  target_index++)
64  {
65  goto_programt::targett t = target_vector[target_index];
66 
67  if(!t->is_goto())
68  continue;
69 
70  goto_programt::const_targett tgt=t->get_target();
71 
72  target_mapt::const_iterator m_it=target_map.find(tgt);
73 
74  if(m_it!=target_map.end())
75  {
76  unsigned j=m_it->second;
77 
78  DATA_INVARIANT(j < target_vector.size(), "in bounds");
79  t->set_target(target_vector[j]);
80  }
81  }
82 }
83 
85  const irep_idt &function_id,
86  goto_programt &goto_program,
87  const goto_programt::const_targett loop_head,
88  const goto_programt::const_targett loop_exit,
89  const unsigned k,
90  const unwind_strategyt unwind_strategy)
91 {
92  std::vector<goto_programt::targett> iteration_points;
93  unwind(
94  function_id,
95  goto_program,
96  loop_head,
97  loop_exit,
98  k,
99  unwind_strategy,
100  iteration_points);
101 }
102 
104  const irep_idt &function_id,
105  goto_programt &goto_program,
106  const goto_programt::const_targett loop_head,
107  const goto_programt::const_targett loop_exit,
108  const unsigned k,
109  const unwind_strategyt unwind_strategy,
110  std::vector<goto_programt::targett> &iteration_points)
111 {
112  PRECONDITION(iteration_points.empty());
113  PRECONDITION(loop_head->location_number < loop_exit->location_number);
114 
115  // rest program after unwound part
116  goto_programt rest_program;
117 
118  if(unwind_strategy==unwind_strategyt::PARTIAL)
119  {
121  rest_program.add(goto_programt::make_skip(loop_head->source_location()));
122 
123  t->location_number=loop_head->location_number;
124 
125  unwind_log.insert(t, loop_head->location_number);
126  }
127  else if(unwind_strategy==unwind_strategyt::CONTINUE)
128  {
129  copy_segment(loop_head, loop_exit, rest_program);
130  }
131  else
132  {
133  PRECONDITION(
134  unwind_strategy == unwind_strategyt::ASSERT_ASSUME ||
135  unwind_strategy == unwind_strategyt::ASSERT_PARTIAL ||
136  unwind_strategy == unwind_strategyt::ASSUME);
137 
138  goto_programt::const_targett t=loop_exit;
139  t--;
140  DATA_INVARIANT(t->is_backwards_goto(), "must be backwards goto");
141 
142  exprt exit_cond = false_exprt(); // default is false
143 
144  if(!t->condition().is_true()) // cond in backedge
145  {
146  exit_cond = boolean_negate(t->condition());
147  }
148  else if(loop_head->is_goto())
149  {
150  if(loop_head->get_target()==loop_exit) // cond in forward edge
151  exit_cond = loop_head->condition();
152  }
153 
154  if(
155  unwind_strategy == unwind_strategyt::ASSERT_ASSUME ||
156  unwind_strategy == unwind_strategyt::ASSERT_PARTIAL)
157  {
158  const std::string loop_number = std::to_string(t->loop_number);
159  source_locationt source_location_annotated = loop_head->source_location();
160  source_location_annotated.set_property_class("unwind");
161  source_location_annotated.set_comment(
162  "unwinding assertion loop " + loop_number);
163  goto_programt::targett assertion = rest_program.add(
164  goto_programt::make_assertion(exit_cond, source_location_annotated));
165  unwind_log.insert(assertion, loop_head->location_number);
166  }
167 
168  if(
169  unwind_strategy == unwind_strategyt::ASSUME ||
170  unwind_strategy == unwind_strategyt::ASSERT_ASSUME)
171  {
172  goto_programt::targett assumption =
173  rest_program.add(goto_programt::make_assumption(
174  exit_cond, loop_head->source_location()));
175  unwind_log.insert(assumption, loop_head->location_number);
176  }
177 
178  }
179 
180  CHECK_RETURN(!rest_program.empty());
181 
182  // to be filled with copies of the loop body
183  goto_programt copies;
184 
185  if(k!=0)
186  {
187  iteration_points.resize(k);
188 
189  // add a goto before the loop exit to guard against 'fall-out'
190 
191  goto_programt::const_targett t_before=loop_exit;
192  t_before--;
193 
194  if(!t_before->is_goto() || !t_before->condition().is_true())
195  {
196  goto_programt::targett t_goto = goto_program.insert_before(
197  loop_exit,
199  goto_program.const_cast_target(loop_exit),
200  true_exprt(),
201  loop_exit->source_location()));
202  t_goto->location_number=loop_exit->location_number;
203 
204  unwind_log.insert(t_goto, loop_exit->location_number);
205  }
206 
207  // add a skip before the loop exit
208 
209  goto_programt::targett t_skip = goto_program.insert_before(
210  loop_exit, goto_programt::make_skip(loop_head->source_location()));
211  t_skip->location_number=loop_head->location_number;
212 
213  unwind_log.insert(t_skip, loop_exit->location_number);
214 
215  // where to go for the next iteration
216  goto_programt::targett loop_iter=t_skip;
217 
218  // record the exit point of first iteration
219  iteration_points[0]=loop_iter;
220 
221  // re-direct any branches that go to loop_head to loop_iter
222 
224  t=goto_program.const_cast_target(loop_head);
225  t!=loop_iter; t++)
226  {
227  if(!t->is_goto())
228  continue;
229 
230  if(t->get_target()==loop_head)
231  t->set_target(loop_iter);
232  }
233 
234  // k-1 additional copies
235  for(unsigned i=1; i<k; i++)
236  {
237  goto_programt tmp_program;
238  copy_segment(loop_head, loop_exit, tmp_program);
239  CHECK_RETURN(!tmp_program.instructions.empty());
240 
241  iteration_points[i]=--tmp_program.instructions.end();
242 
243  copies.destructive_append(tmp_program);
244  }
245  }
246  else
247  {
248  // insert skip for loop body
249 
250  goto_programt::targett t_skip = goto_program.insert_before(
251  loop_head, goto_programt::make_skip(loop_head->source_location()));
252  t_skip->location_number=loop_head->location_number;
253 
254  unwind_log.insert(t_skip, loop_head->location_number);
255 
256  // redirect gotos into loop body
257  for(auto &instruction : goto_program.instructions)
258  {
259  if(!instruction.is_goto())
260  continue;
261 
262  goto_programt::const_targett t = instruction.get_target();
263 
264  if(t->location_number>=loop_head->location_number &&
265  t->location_number<loop_exit->location_number)
266  {
267  instruction.set_target(t_skip);
268  }
269  }
270 
271  // delete loop body
272  goto_program.instructions.erase(loop_head, loop_exit);
273  }
274 
275  // after unwound part
276  copies.destructive_append(rest_program);
277 
278  // now insert copies before loop_exit
279  goto_program.destructive_insert(loop_exit, copies);
280 }
281 
283  const irep_idt &function_id,
284  goto_programt &goto_program,
285  const unwindsett &unwindset,
286  const unwind_strategyt unwind_strategy)
287 {
288  for(goto_programt::const_targett i_it=goto_program.instructions.begin();
289  i_it!=goto_program.instructions.end();)
290  {
291 #ifdef DEBUG
292  std::cout << "Instruction:\n";
293  i_it->output(std::cout);
294 #endif
295 
296  if(!i_it->is_backwards_goto())
297  {
298  i_it++;
299  continue;
300  }
301 
302  PRECONDITION(!function_id.empty());
303  const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it);
304 
305  auto limit=unwindset.get_limit(loop_id, 0);
306 
307  if(!limit.has_value())
308  {
309  // no unwinding given
310  i_it++;
311  continue;
312  }
313 
314  goto_programt::const_targett loop_head=i_it->get_target();
315  goto_programt::const_targett loop_exit=i_it;
316  loop_exit++;
317  CHECK_RETURN(loop_exit != goto_program.instructions.end());
318 
319  unwind(
320  function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
321 
322  // necessary as we change the goto program in the previous line
323  i_it=loop_exit;
324  }
325 }
326 
328  goto_functionst &goto_functions,
329  const unwindsett &unwindset,
330  const unwind_strategyt unwind_strategy)
331 {
332  for(auto &gf_entry : goto_functions.function_map)
333  {
334  goto_functionst::goto_functiont &goto_function = gf_entry.second;
335 
336  if(!goto_function.body_available())
337  continue;
338 
339 #ifdef DEBUG
340  std::cout << "Function: " << gf_entry.first << '\n';
341 #endif
342 
343  goto_programt &goto_program=goto_function.body;
344 
345  unwind(gf_entry.first, goto_program, unwindset, unwind_strategy);
346  }
347 }
348 
349 // call after calling goto_functions.update()!
351 {
352  json_objectt json_result;
353  json_arrayt &json_unwound=json_result["unwound"].make_array();
354 
355  for(location_mapt::const_iterator it=location_map.begin();
356  it!=location_map.end(); it++)
357  {
358  goto_programt::const_targett target=it->first;
359  unsigned location_number=it->second;
360 
361  json_objectt object{
362  {"originalLocationNumber", json_numbert(std::to_string(location_number))},
363  {"newLocationNumber",
364  json_numbert(std::to_string(target->location_number))}};
365 
366  json_unwound.push_back(std::move(object));
367  }
368 
369  return std::move(json_result);
370 }
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
const source_locationt & source_location() const
Definition: expr.h:231
The Boolean constant false.
Definition: std_expr.h:3064
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:945
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:626
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:792
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:799
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:692
unwind_strategyt
Definition: unwind.h:25
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:327
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:84
unwind_logt unwind_log
Definition: unwind.h:115
jsont & push_back(const jsont &json)
Definition: json.h:212
Definition: json.h:27
json_arrayt & make_array()
Definition: json.h:418
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
The Boolean constant true.
Definition: std_expr.h:3055
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:191
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:129
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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
jsont output_log_json() const
Definition: unwind.cpp:350
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.