cprover
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  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  {
131  goto_programt::const_targett t=loop_exit;
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
158  UNREACHABLE;
159 
160  new_t->source_location=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 
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 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
goto_unwindt::unwind_strategyt
unwind_strategyt
Definition: unwind.h:24
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
goto_unwindt::unwind_strategyt::CONTINUE
@ CONTINUE
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:826
exprt
Base class for all expressions.
Definition: expr.h:54
goto_unwindt::unwind_strategyt::ASSERT
@ ASSERT
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
goto_unwindt::unwind
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
jsont
Definition: json.h:27
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
json_arrayt
Definition: json.h:165
goto_unwindt::unwind_strategyt::PARTIAL
@ PARTIAL
json_objectt
Definition: json.h:300
unwindsett::get_limit
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:72
goto_programt::loop_id
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:819
goto_unwindt::unwind_strategyt::ASSUME
@ ASSUME
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:706
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
goto_unwindt::unwind_logt::insert
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:92
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:47
unwindsett
Definition: unwindset.h:23
goto_unwindt::unwind_logt::output_log_json
jsont output_log_json() const
Definition: unwind.cpp:337
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
unwind.h
Loop unwinding.
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:125
goto_unwindt::operator()
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:314
dstringt::empty
bool empty() const
Definition: dstring.h:88
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
goto_unwindt::unwind_logt::location_map
location_mapt location_map
Definition: unwind.h:101
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
expr_util.h
Deprecated expression utility functions.
goto_unwindt::copy_segment
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:26
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
goto_programt::const_cast_target
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:656
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
unwindset.h
Loop unwinding.
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
goto_unwindt::unwind_log
unwind_logt unwind_log
Definition: unwind.h:104