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 #include <util/string_utils.h>
22 
24 
25 #include "loop_utils.h"
26 
28  const goto_programt::const_targett start,
29  const goto_programt::const_targett end, // exclusive
30  goto_programt &goto_program) // result
31 {
32  assert(start->location_number<end->location_number);
33  assert(goto_program.empty());
34 
35  // build map for branch targets inside the loop
36  typedef std::map<goto_programt::const_targett, unsigned> 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());
47  assert(target_vector.empty());
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  assert(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();
62  target_index++)
63  {
64  goto_programt::targett t = target_vector[target_index];
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  assert(j<target_vector.size());
78  t->set_target(target_vector[j]);
79  }
80  }
81 }
82 
84  const irep_idt &function_id,
85  goto_programt &goto_program,
86  const goto_programt::const_targett loop_head,
87  const goto_programt::const_targett loop_exit,
88  const unsigned k,
89  const unwind_strategyt unwind_strategy)
90 {
91  std::vector<goto_programt::targett> iteration_points;
92  unwind(
93  function_id,
94  goto_program,
95  loop_head,
96  loop_exit,
97  k,
98  unwind_strategy,
99  iteration_points);
100 }
101 
103  const irep_idt &function_id,
104  goto_programt &goto_program,
105  const goto_programt::const_targett loop_head,
106  const goto_programt::const_targett loop_exit,
107  const unsigned k,
108  const unwind_strategyt unwind_strategy,
109  std::vector<goto_programt::targett> &iteration_points)
110 {
111  assert(iteration_points.empty());
112  assert(loop_head->location_number<loop_exit->location_number);
113 
114  // rest program after unwound part
115  goto_programt rest_program;
116 
117  if(unwind_strategy==unwind_strategyt::PARTIAL)
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  }
126  else if(unwind_strategy==unwind_strategyt::CONTINUE)
127  {
128  copy_segment(loop_head, loop_exit, rest_program);
129  }
130  else
131  {
132  goto_programt::const_targett t=loop_exit;
133  t--;
134  assert(t->is_backwards_goto());
135 
136  exprt exit_cond = false_exprt(); // default is false
137 
138  if(!t->get_condition().is_true()) // cond in backedge
139  {
140  exit_cond = boolean_negate(t->get_condition());
141  }
142  else if(loop_head->is_goto())
143  {
144  if(loop_head->get_target()==loop_exit) // cond in forward edge
145  exit_cond = loop_head->get_condition();
146  }
147 
149 
150  if(unwind_strategy==unwind_strategyt::ASSERT)
151  {
152  new_t = rest_program.add(goto_programt::make_assertion(exit_cond));
153  }
154  else if(unwind_strategy==unwind_strategyt::ASSUME)
155  {
156  new_t = rest_program.add(goto_programt::make_assumption(exit_cond));
157  }
158  else
159  UNREACHABLE;
160 
161  new_t->source_location=loop_head->source_location;
162  new_t->location_number=loop_head->location_number;
163  unwind_log.insert(new_t, loop_head->location_number);
164  }
165 
166  assert(!rest_program.empty());
167 
168  // to be filled with copies of the loop body
169  goto_programt copies;
170 
171  if(k!=0)
172  {
173  iteration_points.resize(k);
174 
175  // add a goto before the loop exit to guard against 'fall-out'
176 
177  goto_programt::const_targett t_before=loop_exit;
178  t_before--;
179 
180  if(!t_before->is_goto() || !t_before->get_condition().is_true())
181  {
182  goto_programt::targett t_goto = goto_program.insert_before(
183  loop_exit,
185  goto_program.const_cast_target(loop_exit),
186  true_exprt(),
187  loop_exit->source_location));
188  t_goto->location_number=loop_exit->location_number;
189 
190  unwind_log.insert(t_goto, loop_exit->location_number);
191  }
192 
193  // add a skip before the loop exit
194 
195  goto_programt::targett t_skip = goto_program.insert_before(
196  loop_exit, goto_programt::make_skip(loop_head->source_location));
197  t_skip->location_number=loop_head->location_number;
198 
199  unwind_log.insert(t_skip, loop_exit->location_number);
200 
201  // where to go for the next iteration
202  goto_programt::targett loop_iter=t_skip;
203 
204  // record the exit point of first iteration
205  iteration_points[0]=loop_iter;
206 
207  // re-direct any branches that go to loop_head to loop_iter
208 
210  t=goto_program.const_cast_target(loop_head);
211  t!=loop_iter; t++)
212  {
213  if(!t->is_goto())
214  continue;
215 
216  if(t->get_target()==loop_head)
217  t->set_target(loop_iter);
218  }
219 
220  // k-1 additional copies
221  for(unsigned i=1; i<k; i++)
222  {
223  goto_programt tmp_program;
224  copy_segment(loop_head, loop_exit, tmp_program);
225  assert(!tmp_program.instructions.empty());
226 
227  iteration_points[i]=--tmp_program.instructions.end();
228 
229  copies.destructive_append(tmp_program);
230  }
231  }
232  else
233  {
234  // insert skip for loop body
235 
236  goto_programt::targett t_skip = goto_program.insert_before(
237  loop_head, goto_programt::make_skip(loop_head->source_location));
238  t_skip->location_number=loop_head->location_number;
239 
240  unwind_log.insert(t_skip, loop_head->location_number);
241 
242  // redirect gotos into loop body
243  Forall_goto_program_instructions(i_it, goto_program)
244  {
245  if(!i_it->is_goto())
246  continue;
247 
248  goto_programt::const_targett t=i_it->get_target();
249 
250  if(t->location_number>=loop_head->location_number &&
251  t->location_number<loop_exit->location_number)
252  {
253  i_it->set_target(t_skip);
254  }
255  }
256 
257  // delete loop body
258  goto_program.instructions.erase(loop_head, loop_exit);
259  }
260 
261  // after unwound part
262  copies.destructive_append(rest_program);
263 
264  // now insert copies before loop_exit
265  goto_program.destructive_insert(loop_exit, copies);
266 }
267 
269  const irep_idt &function_id,
270  goto_programt &goto_program,
271  const unwindsett &unwindset,
272  const unwind_strategyt unwind_strategy)
273 {
274  for(goto_programt::const_targett i_it=goto_program.instructions.begin();
275  i_it!=goto_program.instructions.end();)
276  {
277 #ifdef DEBUG
278  symbol_tablet st;
279  namespacet ns(st);
280  std::cout << "Instruction:\n";
281  goto_program.output_instruction(ns, function_id, std::cout, *i_it);
282 #endif
283 
284  if(!i_it->is_backwards_goto())
285  {
286  i_it++;
287  continue;
288  }
289 
290  PRECONDITION(!function_id.empty());
291  const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it);
292 
293  auto limit=unwindset.get_limit(loop_id, 0);
294 
295  if(!limit.has_value())
296  {
297  // no unwinding given
298  i_it++;
299  continue;
300  }
301 
302  goto_programt::const_targett loop_head=i_it->get_target();
303  goto_programt::const_targett loop_exit=i_it;
304  loop_exit++;
305  assert(loop_exit!=goto_program.instructions.end());
306 
307  unwind(
308  function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
309 
310  // necessary as we change the goto program in the previous line
311  i_it=loop_exit;
312  }
313 }
314 
316  goto_functionst &goto_functions,
317  const unwindsett &unwindset,
318  const unwind_strategyt unwind_strategy)
319 {
320  Forall_goto_functions(it, goto_functions)
321  {
322  goto_functionst::goto_functiont &goto_function=it->second;
323 
324  if(!goto_function.body_available())
325  continue;
326 
327 #ifdef DEBUG
328  std::cout << "Function: " << it->first << '\n';
329 #endif
330 
331  goto_programt &goto_program=goto_function.body;
332 
333  unwind(it->first, goto_program, unwindset, unwind_strategy);
334  }
335 }
336 
337 // call after calling goto_functions.update()!
339 {
340  json_objectt json_result;
341  json_arrayt &json_unwound=json_result["unwound"].make_array();
342 
343  for(location_mapt::const_iterator it=location_map.begin();
344  it!=location_map.end(); it++)
345  {
346  goto_programt::const_targett target=it->first;
347  unsigned location_number=it->second;
348 
349  json_objectt object{
350  {"originalLocationNumber", json_numbert(std::to_string(location_number))},
351  {"newLocationNumber",
352  json_numbert(std::to_string(target->location_number))}};
353 
354  json_unwound.push_back(std::move(object));
355  }
356 
357  return std::move(json_result);
358 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
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:20
goto_unwindt::unwind_strategyt
unwind_strategyt
Definition: unwind.h:26
string_utils.h
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
goto_unwindt::unwind_strategyt::CONTINUE
@ CONTINUE
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
exprt
Base class for all expressions.
Definition: expr.h:53
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:55
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:83
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:998
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:73
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:755
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:92
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:639
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
goto_unwindt::unwind_logt::insert
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:94
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
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:41
unwindsett
Definition: unwindset.h:24
goto_unwindt::unwind_logt::output_log_json
jsont output_log_json() const
Definition: unwind.cpp:338
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
unwind.h
Loop unwinding.
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:127
goto_unwindt::operator()
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:315
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:3964
goto_unwindt::unwind_logt::location_map
location_mapt location_map
Definition: unwind.h:103
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
loop_utils.h
Helper functions for k-induction and loop invariants.
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
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:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:589
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:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
goto_unwindt::unwind_log
unwind_logt unwind_log
Definition: unwind.h:106