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/std_expr.h>
20 #include <util/string_utils.h>
22 
23 #include "loop_utils.h"
24 
26  const goto_programt::const_targett start,
27  const goto_programt::const_targett end, // exclusive
28  goto_programt &goto_program) // result
29 {
30  assert(start->location_number<end->location_number);
31  assert(goto_program.empty());
32 
33  // build map for branch targets inside the loop
34  typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
35  target_mapt target_map;
36 
37  unsigned i=0;
38 
39  for(goto_programt::const_targett t=start; t!=end; t++, i++)
40  target_map[t]=i;
41 
42  // make a copy
43  std::vector<goto_programt::targett> target_vector;
44  target_vector.reserve(target_map.size());
45  assert(target_vector.empty());
46 
47  for(goto_programt::const_targett t=start; t!=end; t++)
48  {
50  *t_new=*t;
51  unwind_log.insert(t_new, t->location_number);
52  target_vector.push_back(t_new); // store copied instruction
53  }
54 
55  assert(goto_program.instructions.size()==target_vector.size());
56 
57  // adjust intra-segment gotos
58  for(std::size_t i=0; i<target_vector.size(); i++)
59  {
60  goto_programt::targett t=target_vector[i];
61 
62  if(!t->is_goto())
63  continue;
64 
65  goto_programt::const_targett tgt=t->get_target();
66 
67  target_mapt::const_iterator m_it=target_map.find(tgt);
68 
69  if(m_it!=target_map.end())
70  {
71  unsigned j=m_it->second;
72 
73  assert(j<target_vector.size());
74  t->set_target(target_vector[j]);
75  }
76  }
77 }
78 
81  const goto_programt::const_targett loop_head,
82  const goto_programt::const_targett loop_exit,
83  const unsigned k,
84  const unwind_strategyt unwind_strategy)
85 {
86  std::vector<goto_programt::targett> iteration_points;
87  unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
88  iteration_points);
89 }
90 
93  const goto_programt::const_targett loop_head,
94  const goto_programt::const_targett loop_exit,
95  const unsigned k,
96  const unwind_strategyt unwind_strategy,
97  std::vector<goto_programt::targett> &iteration_points)
98 {
99  assert(iteration_points.empty());
100  assert(loop_head->location_number<loop_exit->location_number);
101 
102  // rest program after unwound part
103  goto_programt rest_program;
104 
105  if(unwind_strategy==unwind_strategyt::PARTIAL)
106  {
107  goto_programt::targett t=rest_program.add_instruction();
108  unwind_log.insert(t, loop_head->location_number);
109 
110  t->make_skip();
111  t->source_location=loop_head->source_location;
112  t->function=loop_head->function;
113  t->location_number=loop_head->location_number;
114  }
115  else if(unwind_strategy==unwind_strategyt::CONTINUE)
116  {
117  copy_segment(loop_head, loop_exit, rest_program);
118  }
119  else
120  {
121  goto_programt::const_targett t=loop_exit;
122  t--;
123  assert(t->is_backwards_goto());
124 
125  exprt exit_cond;
126  exit_cond.make_false(); // default is false
127 
128  if(!t->guard.is_true()) // cond in backedge
129  {
130  exit_cond=t->guard;
131  exit_cond.make_not();
132  }
133  else if(loop_head->is_goto())
134  {
135  if(loop_head->get_target()==loop_exit) // cond in forward edge
136  exit_cond=loop_head->guard;
137  }
138 
139  goto_programt::targett new_t=rest_program.add_instruction();
140 
141  if(unwind_strategy==unwind_strategyt::ASSERT)
142  new_t->make_assertion(exit_cond);
143  else if(unwind_strategy==unwind_strategyt::ASSUME)
144  new_t->make_assumption(exit_cond);
145  else
146  UNREACHABLE;
147 
148  new_t->source_location=loop_head->source_location;
149  new_t->function=loop_head->function;
150  new_t->location_number=loop_head->location_number;
151  unwind_log.insert(new_t, loop_head->location_number);
152  }
153 
154  assert(!rest_program.empty());
155 
156  // to be filled with copies of the loop body
157  goto_programt copies;
158 
159  if(k!=0)
160  {
161  iteration_points.resize(k);
162 
163  // add a goto before the loop exit to guard against 'fall-out'
164 
165  goto_programt::const_targett t_before=loop_exit;
166  t_before--;
167 
168  if(!t_before->is_goto() || !t_before->guard.is_true())
169  {
171  unwind_log.insert(t_goto, loop_exit->location_number);
172 
173  t_goto->make_goto(goto_program.const_cast_target(loop_exit));
174  t_goto->source_location=loop_exit->source_location;
175  t_goto->function=loop_exit->function;
176  t_goto->guard=true_exprt();
177  t_goto->location_number=loop_exit->location_number;
178  }
179 
180  // add a skip before the loop exit
181 
183  unwind_log.insert(t_skip, loop_exit->location_number);
184 
185  t_skip->make_skip();
186  t_skip->source_location=loop_head->source_location;
187  t_skip->function=loop_head->function;
188  t_skip->location_number=loop_head->location_number;
189 
190  // where to go for the next iteration
191  goto_programt::targett loop_iter=t_skip;
192 
193  // record the exit point of first iteration
194  iteration_points[0]=loop_iter;
195 
196  // re-direct any branches that go to loop_head to loop_iter
197 
199  t=goto_program.const_cast_target(loop_head);
200  t!=loop_iter; t++)
201  {
202  if(!t->is_goto())
203  continue;
204 
205  if(t->get_target()==loop_head)
206  t->set_target(loop_iter);
207  }
208 
209  // k-1 additional copies
210  for(unsigned i=1; i<k; i++)
211  {
212  goto_programt tmp_program;
213  copy_segment(loop_head, loop_exit, tmp_program);
214  assert(!tmp_program.instructions.empty());
215 
216  iteration_points[i]=--tmp_program.instructions.end();
217 
218  copies.destructive_append(tmp_program);
219  }
220  }
221  else
222  {
223  // insert skip for loop body
224 
226  unwind_log.insert(t_skip, loop_head->location_number);
227 
228  t_skip->make_skip();
229  t_skip->source_location=loop_head->source_location;
230  t_skip->function=loop_head->function;
231  t_skip->location_number=loop_head->location_number;
232 
233  // redirect gotos into loop body
235  {
236  if(!i_it->is_goto())
237  continue;
238 
239  goto_programt::const_targett t=i_it->get_target();
240 
241  if(t->location_number>=loop_head->location_number &&
242  t->location_number<loop_exit->location_number)
243  {
244  i_it->set_target(t_skip);
245  }
246  }
247 
248  // delete loop body
249  goto_program.instructions.erase(loop_head, loop_exit);
250  }
251 
252  // after unwound part
253  copies.destructive_append(rest_program);
254 
255  // now insert copies before loop_exit
256  goto_program.destructive_insert(loop_exit, copies);
257 }
258 
261  const unwindsett &unwindset,
262  const unwind_strategyt unwind_strategy)
263 {
265  i_it!=goto_program.instructions.end();)
266  {
267 #ifdef DEBUG
268  symbol_tablet st;
269  namespacet ns(st);
270  std::cout << "Instruction:\n";
271  goto_program.output_instruction(ns, "", std::cout, *i_it);
272 #endif
273 
274  if(!i_it->is_backwards_goto())
275  {
276  i_it++;
277  continue;
278  }
279 
280  const irep_idt func=i_it->function;
281  assert(!func.empty());
282 
283  const irep_idt loop_id=
284  id2string(func) + "." + std::to_string(i_it->loop_number);
285 
286  auto limit=unwindset.get_limit(loop_id, 0);
287 
288  if(!limit.has_value())
289  {
290  // no unwinding given
291  i_it++;
292  continue;
293  }
294 
295  goto_programt::const_targett loop_head=i_it->get_target();
296  goto_programt::const_targett loop_exit=i_it;
297  loop_exit++;
298  assert(loop_exit!=goto_program.instructions.end());
299 
300  unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
301 
302  // necessary as we change the goto program in the previous line
303  i_it=loop_exit;
304  }
305 }
306 
308  goto_functionst &goto_functions,
309  const unwindsett &unwindset,
310  const unwind_strategyt unwind_strategy)
311 {
312  Forall_goto_functions(it, goto_functions)
313  {
314  goto_functionst::goto_functiont &goto_function=it->second;
315 
316  if(!goto_function.body_available())
317  continue;
318 
319 #ifdef DEBUG
320  std::cout << "Function: " << it->first << '\n';
321 #endif
322 
323  goto_programt &goto_program=goto_function.body;
324 
325  unwind(goto_program, unwindset, unwind_strategy);
326  }
327 }
328 
329 // call after calling goto_functions.update()!
331 {
332  json_objectt json_result;
333  json_arrayt &json_unwound=json_result["unwound"].make_array();
334 
335  for(location_mapt::const_iterator it=location_map.begin();
336  it!=location_map.end(); it++)
337  {
338  json_objectt &object=json_unwound.push_back().make_object();
339 
340  goto_programt::const_targett target=it->first;
341  unsigned location_number=it->second;
342 
343  object["originalLocationNumber"]=json_numbert(std::to_string(
344  location_number));
345  object["newLocationNumber"]=json_numbert(std::to_string(
346  target->location_number));
347  }
348 
349  return json_result;
350 }
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:92
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
Goto Programs with Functions.
Definition: json.h:23
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:407
json_arrayt & make_array()
Definition: json.h:284
unwind_strategyt
Definition: unwind.h:27
jsont & push_back(const jsont &json)
Definition: json.h:163
The boolean constant true.
Definition: std_expr.h:4488
instructionst::iterator targett
Definition: goto_program.h:397
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:25
location_mapt location_map
Definition: unwind.h:101
Helper functions for k-induction and loop invariants.
Loop unwinding.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:307
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
jsont output_log_json() const
Definition: unwind.cpp:330
void make_false()
Definition: expr.cpp:150
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
Definition: goto_program.h:590
#define UNREACHABLE
Definition: invariant.h:250
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
unwind_logt unwind_log
Definition: unwind.h:104
json_objectt & make_object()
Definition: json.h:290
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:64
void unwind(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:79
bool empty() const
Definition: dstring.h:61